Theorem MulEquiv.comp_left_injective

Modification history

2025-01-15 21:51
Mathlib/Algebra/Group/Equiv/Basic.lean
chore(Algebra/Group/Equiv): split into `Defs` and `Basic` (#20712) …
Modified MulEquiv.comp_left_injectiveView on Github →
2024-02-14 08:30
Mathlib/Algebra/Group/Equiv/Basic.lean
feat(Algebra/Group): Miscellaneous lemmas (#9387) …
Added MulEquiv.comp_left_injectiveView on Github →