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 <597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib