Theorem Ordinal.isPrincipal_opow_iff_omega0_opow_eq_self

Modification history

2026-10-17 11:31
Mathlib/SetTheory/Ordinal/Principal.lean
feat(SetTheory/Ordinal): classify exponential principal ordinals (#43633) …
Added Ordinal.isPrincipal_opow_iff_omega0_opow_eq_selfView on Github →