mathlib3
d6f337df - feat(set_theory/ordinal_arithmetic): The derivative of multiplication (#12202)

Commit

3 years ago

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

Author

vihdzp

Parents