[Merged by Bors] - feat(RingTheory/Nilpotents): basic MulOpposite lemmas for IsNilpotent/IsReduced
#35476
Triggered via pull request
August 11, 2026 11:20
mathlib-bors[bot]
mathlib-bors[bot]
edited
#42625
Status
Skipped
Total duration
–
Artifacts
–
check_pr_titles.yaml
on: pull_request_target
check_title
0s