Theorem Ordinal.IsInitial.principal_opow

Modification history

2025-03-17 11:54

Mathlib/SetTheory/Cardinal/Arithmetic.lean

refactor(SetTheory/Cardinal/Ordinal): move results (#21857) …

Modified Ordinal.IsInitial.principal_opow View on Github →

2024-12-16 00:26

Mathlib/SetTheory/Cardinal/Arithmetic.lean

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

Added Ordinal.IsInitial.principal_opow View on Github →