gaussNorm_C — Mathlib

English

For r ∈ R, gaussNorm_C asserts (C r).gaussNorm v c = v r under appropriate assumptions.

Русский

Для элемента r ∈ R гауссова норма константы C r равна v r в подходящих предположениях.

LaTeX

$$gaussNorm_C [ZeroHomClass F R ℝ] (r) : (C r).gaussNorm v c = v r$$

Lean4

@[simp]
theorem gaussNorm_C [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) : (C r).gaussNorm v c = v r := by
  simp [← Polynomial.coe_C, hc]

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