isUnit_pow_succ_iff — Mathlib

English

Let M be a monoid. For any a ∈ M and any n ∈ ℕ, a^(n+1) is a unit if and only if a is a unit.

Русский

Пусть M — моноид. Для любого a ∈ M и любого n ∈ ℕ, a^(n+1) является единицей тогда и только тогда, когда a является единицей.

LaTeX

$$$\\\\forall M [Monoid M], \\\\forall a \\\\in M, \\\\forall n \\\\in \\\\mathbb{N}, \\\\ IsUnit(a^{n+1}) \\\\iff IsUnit(a)$$$

Lean4

@[to_additive]
theorem isUnit_pow_succ_iff : IsUnit (a ^ (n + 1)) ↔ IsUnit a :=
  isUnit_pow_iff n.succ_ne_zero

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