English
Let I be an ideal in a commutative semiring R and n a natural number. Then I^n = ⊤ if and only if I = ⊤ or n = 0. In particular, I^0 = ⊤ and if n > 0 and I ≠ ⊤, then I^n ≠ ⊤.
Русский
Пусть I — идеал кольца R, коммутативного полугруппы, и n — натуральное число. Тогда I^n = ⊤ тогда и только тогда, когда I = ⊤ или n = 0. В частности, I^0 = ⊤, а если n > 0 и I ≠ ⊤, то I^n ≠ ⊤.
LaTeX
$$$ I^n = \\top \\ \iff\\ I = \\top \\ \\lor\\ n = 0 $$$
Lean4
@[simp]
theorem pow_eq_top_iff {n : ℕ} : I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0 :=
by
refine
⟨fun h ↦ or_iff_not_imp_right.mpr fun hn ↦ (eq_top_iff_one _).mpr <| pow_le_self hn <| (eq_top_iff_one _).mp h, ?_⟩
rintro (h | h)
· rw [h, top_pow]
· rw [h, pow_zero, one_eq_top]
