Theorem Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le
Modification history
2024-11-14 01:17
Mathlib/SetTheory/Cardinal/Arithmetic.lean
feat(SetTheory/Cardinal/Arithmetic): fix namespace of `mk_iUnion_Ordinal_le_of_le` (#18541) …
Deleted Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_leView on Github →