isUnit_pow_iff_of_not_isUnit — Mathlib

English

If a is not a unit, then a^n is a unit if and only if n = 0.

Русский

Если a не является единицей, то a^n единица тогда и только тогда, когда n = 0.

LaTeX

$$$\\\\lnot \\\\operatorname{IsUnit}(a) \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, \\\\operatorname{IsUnit}(a^n) \\\\iff n = 0$$$

Lean4

theorem isUnit_pow_iff_of_not_isUnit (hx : ¬IsUnit a) {n : ℕ} : IsUnit (a ^ n) ↔ n = 0 := by
  rcases n with (_ | n) <;> simp [hx]

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