mathlib
0aa0bc8f - feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270)

Commit

4 years ago

feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270) We prove that the derivative of `(+) a` evaluated at `b` is given by `a * ω + b`.

Author

vihdzp

Parents

e60ca6b4

mathlib 0aa0bc8f - feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270)

mathlib
0aa0bc8f - feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270)