cast_pow_eq_one — Mathlib

English

Let R be a semiring of characteristic zero. For any a ∈ ℕ and any n ≠ 0, (a in R)^n = 1 if and only if a = 1.

Русский

Пусть R — полупрямое кольцо с характеристикой нуля. Для любого a ∈ ℕ и любого n ≠ 0 выполнено (a in R)^n = 1 тогда и только тогда a = 1.

LaTeX

$$$(a : R)^n = 1 \\iff a = 1$ при $n \\neq 0$$$

Lean4

@[simp]
theorem cast_pow_eq_one {a : ℕ} (hn : n ≠ 0) : (a : R) ^ n = 1 ↔ a = 1 := by simp [← cast_pow, cast_eq_one, hn]

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