Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-25 20:23
76f1b464
View on Github →
chore: remove duplicate
Ordinal.deriv_id_of_nfp_id
(
#30893
)
Estimated changes
Modified
Mathlib/SetTheory/Ordinal/FixedPoint.lean
deleted
theorem
Ordinal.deriv_id_of_nfp_id