Theorem Ordinal.deriv_eq_id_of_nfp_eq_id

Modification history