eq_bot_or_top — Mathlib

English

Every ideal in a division semiring is either ⊥ or ⊤.

Русский

Каждый идеал в дивизионном полугруппе кольца равен либо ⊥, либо ⊤.

LaTeX

$$$I = \\\\perp \\\\lor I = \\\\top$$$

Lean4

/-- All ideals in a division (semi)ring are trivial. -/
theorem eq_bot_or_top : I = ⊥ ∨ I = ⊤ := by
  rw [or_iff_not_imp_right]
  change _ ≠ _ → _
  rw [Ideal.ne_top_iff_one]
  intro h1
  rw [eq_bot_iff]
  intro r hr
  by_cases H : r = 0; · simpa
  simpa [H, h1] using I.mul_mem_left r⁻¹ hr

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