dvd_pow_self_iff — Mathlib

English

In a commutative monoid, x divides x^n iff n ≠ 0 or x is a unit.

Русский

В коммутативном моноиде x делит x^n тогда, когда n ≠ 0 или x является единицей.

LaTeX

$$$$\operatorname{IsUnit}(x) \\Rightarrow \quad x \mid x^{n} \quad \text{iff} \quad (n \neq 0) \lor \operatorname{IsUnit}(x).$$$$

Lean4

@[simp]
theorem dvd_pow_self_iff {x : α} {n : ℕ} : x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · simp [isUnit_iff_dvd_one]
  · simp [hn, dvd_pow_self]

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