ValuationSubring.exists_mul_pow_inv_mem_of_finiteDimensional_adjoin
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_mul_pow_inv_mem_of_finiteDimensional_adjoin
open PolynomialLean source · statement
theorem _root_.ValuationSubring.exists_mul_pow_inv_mem_of_finiteDimensional_adjoin
{L : Type*} [Field L] {F : Type*} [Field F] [Algebra L F]
(f : F) [FiniteDimensional (IntermediateField.adjoin L ({f} : Set F)) F]
(u : F)
(h₁ : ∀ V : ValuationSubring F, (∀ a : L, algebraMap L F a ∈ V) → f ∈ V → u ∈ V) :
∃ m : ℕ, ∀ V : ValuationSubring F, (∀ a : L, algebraMap L F a ∈ V) → f ∉ V →
u * (f ^ m)⁻¹ ∈ V