single_zpow — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{single}(n,1) = \mathrm{single}(1,1)^n$ for all $n\in\mathbb{Z}$, interpreted via zpow.$$

Lean4

theorem single_zpow (n : ℤ) : single (n : ℤ) (1 : F) = single (1 : ℤ) 1 ^ n := by
  match n with
  | (n : ℕ) => apply single_one_eq_pow
  | -(n + 1 : ℕ) =>
    rw [← Nat.cast_one, ← inv_one, single_inv _ one_ne_zero, zpow_neg, ← Nat.cast_one, Nat.cast_one, inv_inj,
      zpow_natCast, single_one_eq_pow, inv_one]

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