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 <5a6b17dbbc661dec6b250b080ab0033de7d56af5@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib