Theorem mul_left_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_left_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_left_inj_of_invertibleView on Github →2023-11-16 14:12
Mathlib/Algebra/Invertible/Defs.lean
style: cleanup some autoImplicits (#8288) …
Modified mul_left_inj_of_invertibleView on Github →