English
Let o be an ordinal. Then o is multiplicatively principal if and only if either o ≤ 2 or o is of the form ω^{ω^{x}} for some x.
Русский
Пусть o — ординал. Тогда o является главным по умножению тогда и только тогда, когда либо o ≤ 2, либо o имеет вид ω^{ω^{x}} для некоторого x.
LaTeX
$$$\operatorname{Principal}(\cdot \ast \cdot)\ o \;\Longleftrightarrow\; o \le 2 \; \lor\; o \in \{ \omega^{\omega^{x}} : x \in \mathrm{Ordinal}\}$$$
Lean4
/-- The main characterization theorem for multiplicative principal ordinals. -/
theorem principal_mul_iff_le_two_or_omega0_opow_opow :
Principal (· * ·) o ↔ o ≤ 2 ∨ o ∈ Set.range (ω ^ ω ^ · : Ordinal → Ordinal) :=
by
refine ⟨fun ho => ?_, ?_⟩
· rcases le_or_gt o 2 with ho₂ | ho₂
· exact Or.inl ho₂
· rcases principal_add_iff_zero_or_omega0_opow.1 (principal_add_of_principal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
· exact (Ordinal.not_lt_zero 2 ho₂).elim
· rcases principal_add_iff_zero_or_omega0_opow.1 (principal_add_of_principal_mul_opow one_lt_omega0 ho) with
(rfl | ⟨b, rfl⟩)
· simp
· exact Or.inr ⟨b, rfl⟩
· rintro (ho₂ | ⟨a, rfl⟩)
· exact principal_mul_of_le_two ho₂
· exact principal_mul_omega0_opow_opow a
