X_pow_eq — Mathlib

English

The nth power of X_s is the monomial with exponent s repeated n times: (X_s)^n = monomial (single s n) 1.

Русский

Степень n X_s равна моному с экспонентой single s n: (X_s)^n = monomial (single s n) 1.

LaTeX

$$$(X_s)^n = \mathrm{monomial}(\mathrm{single}(s,n), 1)$$$

Lean4

theorem X_pow_eq (s : σ) (n : ℕ) : (X s : MvPowerSeries σ R) ^ n = monomial (single s n) 1 := by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

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