Commit 2024-08-23 03:53 b5972545
View on Github →feat(RingTheory/Derivation): define Differential and DifferentialAlgebra typeclasses (#14699)
Define a typeclass Differential of CommRings with a chosen Derivation, a notation for that derivation, and a DifferentialAlgebra for Algerbas on differential rings whose algebraMap commutes with the derivation.