Module

ValuationSubring_henselianLocalRing_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_henselianLocalRing_of_isAlgClosed

4 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring henselian Local Ring of is Alg Closed

Imports5

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.Henselian
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.Algebra.Polynomial.Div
Mathlib.Tactic.LinearCombination

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

mem_of_isRoot_map

L36 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed.ValuationSubring.HenselianOfAlgClosed.mem_of_isRoot_map

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace HenselianOfAlgClosed
open _root_.ValuationSubring
variable {L : Type*} [Field L] (A : ValuationSubring L)

Lean source · statement

theorem mem_of_isRoot_map {f : A[X]} (hf : f.Monic) {r : L} (hr : (f.map A.subtype).IsRoot r) :
    r ∈ A

theorem

exists_isRoot_and_sub_mem

L86 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed.ValuationSubring.HenselianOfAlgClosed.exists_isRoot_and_sub_mem

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace HenselianOfAlgClosed
open _root_.ValuationSubring
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]

Lean source · statement

theorem exists_isRoot_and_sub_mem :
    ∀ (n : ℕ) (f : A[X]), f.Monic → f.natDegree = n →
      ∀ a₀ : A, f.eval a₀ ∈ maximalIdeal A → ∃ a : A, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal A

theorem

henselianLocalRing

L131 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed.ValuationSubring.HenselianOfAlgClosed.henselianLocalRing

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
namespace HenselianOfAlgClosed
open _root_.ValuationSubring
variable {L : Type*} [Field L] (A : ValuationSubring L)
variable [IsAlgClosed L]

Lean source · full declaration

theorem henselianLocalRing : HenselianLocalRing A where
  toIsLocalRing := inferInstance
  is_henselian f hf a₀ h₀ _ := exists_isRoot_and_sub_mem A f.natDegree f hf rfl a₀ h₀

theorem

henselianLocalRing_of_isAlgClosed

L137 ↗

ValuationSubring.henselianLocalRing_of_isAlgClosed

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_henselianLocalRing_of_isAlgClosed
open IsLocalRing Polynomial

Lean source · statement

theorem _root_.ValuationSubring.henselianLocalRing_of_isAlgClosed {L : Type*} [Field L]
  [IsAlgClosed L] (A : ValuationSubring L) : HenselianLocalRing A

Module documentation

Valuation Subring henselian Local Ring of is Alg Closed

Declarations

mem_of_isRoot_map

exists_isRoot_and_sub_mem

henselianLocalRing

henselianLocalRing_of_isAlgClosed