monic_monomial_eq — Mathlib

English

The monomial with exponent m and coefficient 1 equals the product across indices: monomial m (1) = ∏_{n,e} X_n^e with m(n)=e.

Русский

Мономиал с экспонентой m и коэффициентом 1 равен произведению по всем индексам: monomial m (1) = ∏_{n,e} X_n^e при m(n)=e.

LaTeX

$$$\mathrm{monomial}(m,1) = \big( m.\prod (n,e \mapsto X_n^{e}) \big)$$$

Lean4

theorem monic_monomial_eq (m) : monomial m (1 : R) = (m.prod fun n e => X n ^ e : MvPolynomial σ R) := by
  simp [monomial_eq]

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