mathlib3

b40c1406 - feat(ring_theory/derivation): A presentation of the Kähler differential module (#17011)

feat(ring_theory/derivation): A presentation of the Kähler differential module (#17011) We add an alternative description of `Ω[S⁄R]`, presenting it as `S` copies of `S` with kernel generated by the relations: 1. `dx + dy = d(x + y)` 2. `x dy + y dx = d(x * y)` 3. `dr = 0` for `r ∈ R` Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>