mathlib

7db9e13b - feat(data/monoid_algebra): ext lemma (#4162)

feat(data/monoid_algebra): ext lemma (#4162) A small lemma that was useful in the Witt vector project. Co-authored by: Johan Commelin <johan@commelin.net> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>