isUnit_pow_iff — Mathlib

English

Let M be a monoid. For any a ∈ M and any n ∈ ℕ with n ≠ 0, a^n is a unit if and only if a is a unit.

Русский

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

LaTeX

$$$\\\\forall M [Monoid M], \\\\forall a \\\\in M, \\\\forall n \\\\in \\\\mathbb{N}, \\\\ n \\\\neq 0 \\\\Rightarrow \\\\operatorname{IsUnit}(a^n) \\\\iff \\\\operatorname{IsUnit}(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem isUnit_pow_iff (hn : n ≠ 0) : IsUnit (a ^ n) ↔ IsUnit a :=
  ⟨fun ⟨u, hu⟩ ↦ (u.ofPow a hn hu.symm).isUnit, IsUnit.pow n⟩

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