single_one_eq_pow — Mathlib

English

For any nonnegative integer n, the monomial at exponent n with coefficient 1 equals the nth power of the monomial at exponent 1 with coefficient 1.

Русский

Для любого неотрицательного целого n моном при степени n и коэффициенте 1 равен n-й степени монома при степени 1 и коэффициенте 1.

LaTeX

$$$\mathrm{single}(n,1) = \mathrm{single}(1,1)^n$ for all $n\in\mathbb{N}$.$$

Lean4

theorem single_one_eq_pow {R : Type*} [Semiring R] (n : ℕ) : single (n : ℤ) (1 : R) = single (1 : ℤ) 1 ^ n := by
  induction n with
  | zero => simp
  | succ n h_ind => rw [← Int.ofNat_add_one_out, pow_succ', ← h_ind, HahnSeries.single_mul_single, one_mul, add_comm]

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