Theorems · Theorem · commutative algebra

Valuation.transcendental_of_ne_one

∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] (A : Type u_2) [inst_1 : CommRing A] {K : Type u_3}
  [inst_2 : Field K] [inst_3 : Algebra A K] {v : Valuation K Γ} [hv : Valuation.IsTrivialOn A v] (y : K),
  y ≠ 0 → v y ≠ 1 → Transcendental A y

For an A-algebra K and a valuation v over K which is trivial on A. If y : K is such that y ≠ 0 and v y ≠ 1, then it is transcendental over A.

Defined in

Mathlib.RingTheory.Valuation.IsTrivialOn

Cited by

0 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderedCommGroupWithZeroCommRingFieldAlgebraValuation.IsTrivialOn