Theorem Commute.isNilpotent_mul_right
Modification history
2025-07-22 20:14
Mathlib/RingTheory/Nilpotent/Defs.lean
fix(NonZeroDivisors): swap left and right (#27224) …
Modified Commute.isNilpotent_mul_rightView on Github →2024-08-01 16:02
Mathlib/RingTheory/Nilpotent/Defs.lean
chore: backports for leanprover/lean4#4814 (part 11) (#15394) …
Modified Commute.isNilpotent_mul_rightView on Github →