English
For a division semiring K, there is a bijection between the ideals of K and the two-element set Fin(2), given by I ↦ 0 if I = ⊥ and 1 otherwise; the inverse sends 0 ↦ ⊥ and 1 ↦ ⊤.
Русский
Для делимого полукольца K существует биекция между идеалами K и двумя элементами Fin(2): I ↦ 0, если I = ⊥, иначе 1; обратная биекция отправляет 0 в ⊥, 1 в ⊤.
LaTeX
$$$\\mathrm{Ideal}(K) \\cong \\mathrm{Fin}(2)$$$
Lean4
/-- A bijection between (left) ideals of a division ring and `{0, 1}`, sending `⊥` to `0`
and `⊤` to `1`. -/
def equivFinTwo [DecidableEq (Ideal K)] : Ideal K ≃ Fin 2
where
toFun := fun I ↦ if I = ⊥ then 0 else 1
invFun := ![⊥, ⊤]
left_inv := fun I ↦ by rcases eq_bot_or_top I with rfl | rfl <;> simp
right_inv := fun i ↦ by fin_cases i <;> simp
