Theorem Ordinal.isLimit_of_principal_add

Modification history

2024-11-12 10:47

Mathlib/SetTheory/Ordinal/Principal.lean

chore(SetTheory/Ordinal/Principal): use `variable` (#18898) …

Modified Ordinal.isLimit_of_principal_add View on Github →

2024-11-01 03:45

Mathlib/SetTheory/Ordinal/Principal.lean

refactor(SetTheory/Ordinal/Principal): fix bad names (#17842) …

Added Ordinal.isLimit_of_principal_add View on Github →