English
A ring R is a simple module over itself iff R is nontrivial and every nonzero element is a unit; i.e., R is a division ring.
Русский
Кольцо R является простым модулем над собой тогда и только тогда, когда R не тривиален и каждый ненулевой элемент является единицей; т.е. R — деление кольца.
LaTeX
$$IsSimpleModule R R \\iff (Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x)$$
Lean4
/-- A ring is a simple module over itself iff it is a division ring. -/
theorem isSimpleModule_self_iff_isUnit : IsSimpleModule R R ↔ Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x :=
isSimpleModule_iff_toSpanSingleton_surjective.trans <|
and_congr_right fun _ ↦
by
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1
have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1
exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩
