Module

ValuationSubring_exists_root_mem_of_monic.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_root_mem_of_monic

1 declaration indexed from sourceView source ↗

Module documentation

Valuation Subring exists root mem of monic

Imports2

Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.Valuation.LocalSubring

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

exists_root_mem_of_monic

L25 ↗

ValuationSubring.exists_root_mem_of_monic

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_root_mem_of_monic

Lean source · statement

theorem _root_.ValuationSubring.exists_root_mem_of_monic {K : Type*} [Field K] [IsAlgClosed K]
    (A : ValuationSubring K) (f : Polynomial A) (hf : f.Monic) (hd : f.natDegree ≠ 0) :
    ∃ x : A, Polynomial.aeval (x : K) f = 0

Module documentation

Valuation Subring exists root mem of monic

Declarations

exists_root_mem_of_monic