Commit 2022-11-15 10:09 b40c1406

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