Theorem Ordinal.card_opow_eq_of_omega0_le_right

Modification history

2024-12-16 00:26

Mathlib/SetTheory/Cardinal/Arithmetic.lean

feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential (#17813) …

Added Ordinal.card_opow_eq_of_omega0_le_right View on Github →