gaussNorm_monomial — Mathlib

English

For a monomial, gaussNorm is v(r) · c^n where n is the degree of the monomial and r its coefficient.

Русский

Для монома gaussNorm = v(r) · c^n, где n — степень монома, r — его коэффициент.

LaTeX

$$gaussNorm_monomial(v,c;n,r) = v r · c^n$$

Lean4

@[simp]
theorem gaussNorm_monomial [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) (n : ℕ) :
    (monomial n r).gaussNorm v c = v r * c ^ n := by simp [← Polynomial.coe_monomial, hc]

Похожие утверждения