trunc_one — Mathlib

English

If the index n is nonzero, the truncation of the constant 1 in the mv power series to degree n is still the constant 1.

Русский

Если показатель степени n не равен нулю, усечение константы 1 в многопеременном формальном степенном ряде остаётся константой 1.

LaTeX

$$$$ \\operatorname{trunc} R n 1 = 1, \\quad \\text{when } n \\neq 0. $$$$

Lean4

@[simp]
theorem trunc_one (n : σ →₀ ℕ) (hnn : n ≠ 0) : trunc R n 1 = 1 :=
  MvPolynomial.ext _ _ fun m ↦ by
    classical
    rw [coeff_trunc, coeff_one]
    split_ifs with H H'
    · subst m
      simp
    · symm
      rw [MvPolynomial.coeff_one]
      exact if_neg (Ne.symm H')
    · symm
      rw [MvPolynomial.coeff_one]
      refine if_neg ?_
      rintro rfl
      apply H
      exact Ne.bot_lt hnn

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