val_zpow_eq_zpow_val — Mathlib

English

For any α with DivisionMonoid structure, and any u ∈ αˣ, and integer n, the equality (u^n : α) = (u : α)^n holds, i.e., underlying of zpow agrees with zpow of underlying.

Русский

Для α со структурой DivisionMonoid и любого u ∈ αˣ и целого n выполняется (u^n : α) = (u : α)^n; то есть переход через подстановку сохраняет zpow.

LaTeX

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

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem val_zpow_eq_zpow_val : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = (u : α) ^ n :=
  (Units.coeHom α).map_zpow

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