Algebra.exists_adjoin_ne_zero_mul_forall_valuationSubring_mem
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace Algebra_exists_adjoin_ne_zero_mul_forall_valuationSubring_mem
open Polynomial
noncomputable sectionLean source · statement
theorem _root_.Algebra.exists_adjoin_ne_zero_mul_forall_valuationSubring_mem
{L : Type*} [Field L] {F : Type*} [Field F] [Algebra L F]
(f : F) [FiniteDimensional (IntermediateField.adjoin L ({f} : Set F)) F]
(z : F) :
∃ q₀ : Algebra.adjoin L ({f} : Set F), q₀ ≠ 0 ∧
∀ V : ValuationSubring F, (∀ a : L, algebraMap L F a ∈ V) → f ∈ V → (q₀ : F) * z ∈ V