Theorem MulEquiv.toEquiv_injective

Modification history

2024-11-19 17:06

Mathlib/Algebra/Group/Equiv/Basic.lean

feat: define instances of `Finite`, `Fintype`, `DecidableEq` for `MulEquiv` (#17057)

Added MulEquiv.toEquiv_injective View on Github →