coe_units_zpow — Mathlib

English

Let u be a unit in the matrix units group M^×. For every integer n, the underlying matrix of u^n equals the nth power of the underlying matrix u.

Русский

Пусть u — единица в группе единиц матричного кольца M^×. Для каждого целого числа n матрица, лежащая в единицах u^n, равна n-й степени матрицы u.

LaTeX

$$$ \forall u \in M^{\times},\forall n \in \mathbb{Z},\ ((u^n) : M) = (u : M)^n $$$

Lean4

@[simp, norm_cast]
theorem coe_units_zpow (u : Mˣ) : ∀ n : ℤ, ((u ^ n : Mˣ) : M) = (u : M) ^ n
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]
  | -[k+1] => by rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]

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