Why `Derivation` for `CommSemiring`

Stream: mathlib4

[Yiming Fu]

I noticed that the definition of Derivation is currently set up for CommSemiring. Why do we need CommSemiring here? I'm trying to prove that the ExteriorAlgebra is a differential graded algebra—that is, a graded algebra equipped with a Derivation. I don't think the CommSemiring assumption is necessary.

[Kenny Lau]

@Yiming Fu #mathlib4 > Generalizing Derivation module

[Yiming Fu]

Thanks, I will see this post!