[Merged by Bors] - feat(Algebra): auxiliary lemmas for flatness over semirings · leanprover-community/mathlib4@bd84f8e