Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_polynomial_map_residue_ne_zero_eval_mul_mem

theorem

exists_polynomial_map_residue_ne_zero_eval_mul_mem

ValuationSubring.exists_polynomial_map_residue_ne_zero_eval_mul_mem

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_polynomial_map_residue_ne_zero_eval_mul_mem
open Polynomial

Lean source · statement

theorem _root_.ValuationSubring.exists_polynomial_map_residue_ne_zero_eval_mul_mem
    {L : Type*} [Field L] (A : ValuationSubring L)
    {F : Type*} [Field F] [Algebra L F]
    (f : F) [FiniteDimensional (IntermediateField.adjoin L ({f} : Set F)) F]
    (z : F) :
    ∃ q : Polynomial A, (q.map (IsLocalRing.residue A)) ≠ 0 ∧
      ∀ V : ValuationSubring F, (∀ a : L, algebraMap L F a ∈ V) → f ∈ V →
        (Polynomial.eval₂ ((algebraMap L F).comp A.subtype) f q) * z ∈ V

ValuationSubring_exists_polynomial_map_residue_ne_zero_eval_mul_mem.lean

Module documentation

Valuation Subring exists polynomial map residue ne zero eval mul mem

exists_polynomial_map_residue_ne_zero_eval_mul_mem

Module documentation

Valuation Subring exists polynomial map residue ne zero eval mul mem

Declarations

exists_polynomial_map_residue_ne_zero_eval_mul_mem