leadingCoeff_esymmAlgHomMonomial — Mathlib

English

For any t: Fin n →₀ ℕ and any n ≤ m, the leading coefficient, with respect to toLex, of the polynomial esymmAlgHomMonomial (Fin m) t r equals r.

Русский

Для любой функции t: Fin n →₀ ℕ и при любом n ≤ m старший коэффициент по отношению к toLex у esymmAlgHomMonomial (Fin m) t r равен r.

LaTeX

$$$\operatorname{leadingCoeff}_{toLex} \big(\operatorname{esymmAlgHomMonomial} (\operatorname{Fin} m) t r\big) = r$$$

Lean4

theorem leadingCoeff_esymmAlgHomMonomial (t : Fin n →₀ ℕ) (hnm : n ≤ m) :
    leadingCoeff toLex (esymmAlgHomMonomial (Fin m) t r) = r := by
  induction t using Finsupp.induction₂ with
  | zero => rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
  | add_single i _ _ _ _
    ih =>
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
      ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left, ih]
    exacts [toLex.injective, toLex_add]

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