Theorems · Theorem · commutative algebra

Polynomial.valuation_aeval_monomial_eq_valuation_pow

∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : CommSemiring A] {B : Type u_3}
  [inst_2 : Ring B] [inst_3 : Algebra A B] {v : Valuation B Γ} [hv : Valuation.IsTrivialOn A v] (w : B) (n : ℕ) {a : A},
  a ≠ 0 → v ((Polynomial.aeval w) ((Polynomial.monomial n) a)) = v w ^ n

Defined in

Mathlib.RingTheory.Valuation.IsTrivialOn

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroCommSemiringRingAlgebraValuation.IsTrivialOn