NYLL
Module

ValuationSubring_isAlgClosed_residueField_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_isAlgClosed_residueField_of_isAlgClosed
1 declaration indexed from sourceView source ↗

Module documentation

Valuation Subring is Alg Closed residue Field of is Alg Closed

Imports10
  • Mathlib.Algebra.Polynomial.Degree.Lemmas
  • Mathlib.Algebra.Polynomial.Eval.Defs
  • Mathlib.Algebra.Polynomial.FieldDivision
  • Mathlib.Algebra.Polynomial.Lifts
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
  • Mathlib.RingTheory.Localization.FractionRing
  • Mathlib.RingTheory.Valuation.LocalSubring
  • Mathlib.RingTheory.Valuation.ValuationSubring
Imported by1

Declarations

theorem

isAlgClosed_residueField_of_isAlgClosed

L32 ↗
ValuationSubring.isAlgClosed_residueField_of_isAlgClosed
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_isAlgClosed_residueField_of_isAlgClosed
Lean source · statement
theorem _root_.ValuationSubring.isAlgClosed_residueField_of_isAlgClosed
    {L : Type*} [Field L] [IsAlgClosed L] (A : ValuationSubring L) :
    IsAlgClosed (IsLocalRing.ResidueField ↥A)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.