Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-11 16:25 d6f337df

View on Github →

feat(set_theory/ordinal_arithmetic): The derivative of multiplication (#12202) We prove that for 0 < a, deriv ((*) a) b = a ^ ω * b.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.deriv_eq_id_of_nfp_eq_id

added theorem ordinal.deriv_mul_eq_opow_omega_mul

added theorem ordinal.deriv_mul_zero

added theorem ordinal.eq_zero_or_opow_omega_le_of_mul_eq_right

deleted theorem ordinal.le_opow_self

added theorem ordinal.left_le_opow

added theorem ordinal.mul_eq_right_iff_opow_omega_dvd

added theorem ordinal.mul_le_right_iff_opow_omega_dvd

added theorem ordinal.nfp_mul_eq_opow_omega

added theorem ordinal.nfp_mul_one

added theorem ordinal.nfp_mul_opow_omega_add

added theorem ordinal.nfp_mul_zero

added theorem ordinal.nfp_zero_mul

added theorem ordinal.opow_one_add

added theorem ordinal.right_le_opow