Theorems · Theorem · commutative algebra

Polynomial.gaussNorm_mul

∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
  IsNonarchimedean ⇑v →
    0 < c →
      ∀ (p q : Polynomial R), Polynomial.gaussNorm v c (p * q) = Polynomial.gaussNorm v c p * Polynomial.gaussNorm v c q

If v is a nonarchimedean absolute value, then the Gauss norm is multiplicative.

Defined in: Mathlib.RingTheory.Polynomial.GaussNorm
Cited by: 1 results in Mathlib
Foundations: Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
Ringstatement and proof · cited by 7,463
Polynomialstatement and proof · cited by 5,681
le_antisymmproof · cited by 2,068
le_of_ltproof · cited by 1,175
AbsoluteValuestatement and proof · cited by 363
IsNonarchimedeanstatement and proof · cited by 77
Polynomial.gaussNormstatement · cited by 20
Polynomial.gaussNorm_mul_leproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.gaussNorm_isAbsoluteValueproof · cited by 0