monic_esymm — Mathlib

English

For every i with i ≤ m, the polynomial esymm (Fin m) R i is monic with respect to the Lex ordering, i.e. its leading coefficient with respect to toLex is 1.

Русский

Для каждого i ≤ m многочлен esymm (Fin m) R i является мономическим по отношению к упорядочению Lex; старшая степень имеет коэффициент 1.

LaTeX

$$$\operatorname{Monic} \text{toLex} \big( \operatorname{esymm} (\operatorname{Fin} m) R i \big)$ при $i \le m$$$

Lean4

theorem monic_esymm {i : ℕ} (him : i ≤ m) : Monic toLex (esymm (Fin m) R i) := by
  cases i with
  | zero =>
    rw [esymm_zero]
    exact monic_one toLex.injective
  | succ i =>
    nontriviality R
    exact (supDegree_monic_esymm him).2

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