Theorem mul_right_inj_of_invertible

Modification history

2024-11-19 10:10
Mathlib/Algebra/Group/Invertible/Defs.lean
chore: fix some left/right injectivity names (#19239) …
Modified mul_right_inj_of_invertibleView on Github →
2023-11-16 17:27
Mathlib/Algebra/Invertible/Defs.lean
chore(Algebra/Invertible/Defs): extract a variable command (#8441) …
Modified mul_right_inj_of_invertibleView on Github →
2023-11-16 14:12
Mathlib/Algebra/Invertible/Defs.lean
style: cleanup some autoImplicits (#8288) …
Modified mul_right_inj_of_invertibleView on Github →
2023-09-06 11:21
Mathlib/Algebra/Invertible.lean
chore: split Mathlib.Algebra.Invertible (#6973) …
Modified mul_right_inj_of_invertibleView on Github →
2023-01-22 01:26
Mathlib/Algebra/Invertible.lean
feat: `=`, `≠`, `<`, and `≤` functionality for `norm_num` (#1568) …
Added mul_right_inj_of_invertibleView on Github →