norm_zpow_isUnit — Mathlib

English

If the exponent n is a unit in ℤ, then ‖a^n‖ = ‖a‖ for all a ∈ E.

Русский

Если показатель n является единичным элементом целых чисел, то для всех a ∈ E выполняется ‖a^n‖ = ‖a‖.

LaTeX

$$$\forall a \in E,\ n \in \mathbb{Z}^{\times} \Rightarrow \|a^n\| = \|a\|$$$

Lean4

@[to_additive norm_isUnit_zsmul]
theorem norm_zpow_isUnit (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖ = ‖a‖ := by
  rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]

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