English
Principal (· + ·) o ⇔ o = 0 ∨ o ∈ { ω^k : k ∈ Ordinal }. (extended form)
Русский
Principial сложения для o ⇔ o = 0 ∨ o ∈ { ω^k : k ∈ Ordinal } (расширенная форма).
LaTeX
$$$Principal(\cdot + \cdot, o) \iff o = 0 \lor o \in \{ \omega^k : k \in \text{Ordinal} \}.$$$
Lean4
theorem principal_mul_iff_mul_left_eq : Principal (· * ·) o ↔ ∀ a, 0 < a → a < o → a * o = o :=
by
refine ⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩
· rcases le_or_gt o 2 with ho | ho
· convert one_mul o
apply le_antisymm
· rw [← lt_succ_iff, succ_one]
exact hao.trans_le ho
· rwa [← succ_le_iff, succ_zero] at ha₀
· exact op_eq_self_of_principal hao (isNormal_mul_right ha₀) h (isSuccLimit_of_principal_mul ho h)
· rcases eq_or_ne a 0 with (rfl | ha)
· dsimp only; rwa [zero_mul]
rw [← Ordinal.pos_iff_ne_zero] at ha
rw [← h a ha hao]
exact (isNormal_mul_right ha).strictMono hbo
