Theorem MulEquivClass.toMulEquiv_injective

Modification history

2023-12-05 18:54
Mathlib/Algebra/Group/Equiv/Basic.lean
feat: Add API for `AlgEquiv`. (#8639)
Added MulEquivClass.toMulEquiv_injectiveView on Github →