Commit 2024-07-18 09:55 93decccd

View on Github →

feat(RingTheory/Derivation/Basic): add lemmas about the derivation of a fraction (#14857) Add lemmas about the derivation of a fraction in a field.

Estimated changes

Modified Mathlib/RingTheory/Derivation/Basic.lean

added theorem Derivation.leibniz_div

added theorem Derivation.leibniz_div_const

modified theorem Derivation.leibniz_inv

added theorem Derivation.leibniz_zpow