Theorem MulEquiv.toEquiv_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.toEquiv_injectiveView on Github →
2024-11-19 17:06
Mathlib/Algebra/Group/Equiv/Basic.lean
feat: define instances of `Finite`, `Fintype`, `DecidableEq` for `MulEquiv` (#17057)
Added MulEquiv.toEquiv_injectiveView on Github →