gaussNorm_monomial

Mathlib.RingTheory.Polynomial.GaussNorm

URI: https://scilib.ai/kg/mathlib#Polynomial.gaussNorm_monomial

← MathLib Explorer

English

The Gauss norm of a monomial is the value at the coefficient times c^n: gaussNorm((monomial n r), v, c) = v(r) · c^n.

Русский

Гауссова норма монома равна v(r) · c^n для monomial n r.

LaTeX

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

Lean4

@[simp]
theorem gaussNorm_monomial [ZeroHomClass F R ℝ] (n : ℕ) (r : R) : (monomial n r).gaussNorm v c = v r * c ^ n := by
  by_cases hr : r = 0 <;> simp [gaussNorm, support_monomial, hr]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru