Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_is_right_regular_iff

Modification history

2022-04-05 09:11
src/algebra/regular/basic.lean
feat(algebra/group/to_additive + algebra/regular/basic): add to_additive for `is_regular` (#12930) …
Modified mul_is_right_regular_iffView on Github →
2021-02-20 17:42
src/algebra/regular.lean
feat(algebra/regular): define regular elements (#6282) …
Added mul_is_right_regular_iffView on Github →