[Merged by Bors] - feat(RingTheory/Nilpotents): basic MulOpposite lemmas for IsNilpotent/IsReduced - #42625

[Merged by Bors] - feat(RingTheory/Nilpotents): basic MulOpposite lemmas for IsNilpotent/IsReduced#42625

vlad902 wants to merge 5 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

vlad902:nilpotent-reduced-muloppositevlad902/mathlib4:nilpotent-reduced-muloppositeCopy head branch name to clipboard