Basic

📁 Source: Mathlib/Algebra/Group/Equiv/Basic.lean

Statistics

Metric	Count
Definitions `addMonoidHomCongrLeft`, `addMonoidHomCongrLeftEquiv`, `addMonoidHomCongrRight`, `addMonoidHomCongrRightEquiv`, `arrowCongr`, `funUnique`, `instUnique`, `ofUnique`, `piCongrRight`, `piUnique`, `inv`, `neg`, `arrowCongr`, `funUnique`, `instUnique`, `monoidHomCongrLeft`, `monoidHomCongrLeftEquiv`, `monoidHomCongrRight`, `monoidHomCongrRightEquiv`, `ofUnique`, `piCongrRight`, `piUnique`	22
Theorems `addMonoidHomCongrLeftEquiv_apply`, `addMonoidHomCongrLeftEquiv_refl`, `addMonoidHomCongrLeftEquiv_symm_apply`, `addMonoidHomCongrLeftEquiv_trans`, `addMonoidHomCongrLeft_apply`, `addMonoidHomCongrLeft_refl`, `addMonoidHomCongrLeft_trans`, `addMonoidHomCongrRightEquiv_apply`, `addMonoidHomCongrRightEquiv_refl`, `addMonoidHomCongrRightEquiv_symm_apply`, `addMonoidHomCongrRightEquiv_trans`, `addMonoidHomCongrRight_apply`, `addMonoidHomCongrRight_refl`, `addMonoidHomCongrRight_trans`, `arrowCongr_apply`, `funUnique_apply`, `funUnique_symm_apply`, `piCongrRight_apply`, `piCongrRight_refl`, `piCongrRight_symm`, `piCongrRight_trans`, `piUnique_apply`, `piUnique_symm_apply`, `symm_addMonoidHomCongrLeft`, `symm_addMonoidHomCongrLeftEquiv`, `symm_addMonoidHomCongrRight`, `symm_addMonoidHomCongrRightEquiv`, `isDedekindFiniteAddMonoid_iff`, `toAddEquiv_injective`, `inv_apply`, `inv_symm`, `neg_apply`, `neg_symm`, `arrowCongr_apply`, `funUnique_apply`, `funUnique_symm_apply`, `monoidHomCongrLeftEquiv_apply`, `monoidHomCongrLeftEquiv_refl`, `monoidHomCongrLeftEquiv_symm_apply`, `monoidHomCongrLeftEquiv_trans`, `monoidHomCongrLeft_apply`, `monoidHomCongrLeft_refl`, `monoidHomCongrLeft_trans`, `monoidHomCongrRightEquiv_apply`, `monoidHomCongrRightEquiv_refl`, `monoidHomCongrRightEquiv_symm_apply`, `monoidHomCongrRightEquiv_trans`, `monoidHomCongrRight_apply`, `monoidHomCongrRight_refl`, `monoidHomCongrRight_trans`, `piCongrRight_apply`, `piCongrRight_refl`, `piCongrRight_symm`, `piCongrRight_trans`, `piUnique_apply`, `piUnique_symm_apply`, `symm_monoidHomCongrLeft`, `symm_monoidHomCongrLeftEquiv`, `symm_monoidHomCongrRight`, `symm_monoidHomCongrRightEquiv`, `isDedekindFiniteMonoid_iff`, `toMulEquiv_injective`	62
Total	84

AddEquiv

Definitions

Name	Category	Theorems
`addMonoidHomCongrLeft` 📖	CompOp	4 math math: `addMonoidHomCongrLeft_apply`, `addMonoidHomCongrLeft_trans`, `addMonoidHomCongrLeft_refl`, `symm_addMonoidHomCongrLeft`
`addMonoidHomCongrLeftEquiv` 📖	CompOp	5 math math: `addMonoidHomCongrLeftEquiv_apply`, `addMonoidHomCongrLeftEquiv_refl`, `symm_addMonoidHomCongrLeftEquiv`, `addMonoidHomCongrLeftEquiv_symm_apply`, `addMonoidHomCongrLeftEquiv_trans`
`addMonoidHomCongrRight` 📖	CompOp	4 math math: `symm_addMonoidHomCongrRight`, `addMonoidHomCongrRight_trans`, `addMonoidHomCongrRight_refl`, `addMonoidHomCongrRight_apply`
`addMonoidHomCongrRightEquiv` 📖	CompOp	5 math math: `addMonoidHomCongrRightEquiv_refl`, `addMonoidHomCongrRightEquiv_symm_apply`, `addMonoidHomCongrRightEquiv_apply`, `addMonoidHomCongrRightEquiv_trans`, `symm_addMonoidHomCongrRightEquiv`
`arrowCongr` 📖	CompOp	1 math math: `arrowCongr_apply`
`funUnique` 📖	CompOp	3 math math: `funUnique_symm_apply`, `LinearEquiv.funUnique_symm_apply`, `funUnique_apply`
`instUnique` 📖	CompOp	—
`ofUnique` 📖	CompOp	—
`piCongrRight` 📖	CompOp	4 math math: `piCongrRight_symm`, `piCongrRight_refl`, `piCongrRight_trans`, `piCongrRight_apply`
`piUnique` 📖	CompOp	2 math math: `piUnique_apply`, `piUnique_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHomCongrLeftEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `addMonoidHomCongrLeftEquiv` `AddMonoidHom.comp` `toAddMonoidHom` `symm` `AddZero.toAdd`	—	—
`addMonoidHomCongrLeftEquiv_refl` 📖	mathematical	—	`addMonoidHomCongrLeftEquiv` `refl` `AddZero.toAdd` `AddZeroClass.toAddZero` `Equiv.refl` `AddMonoidHom` `AddMonoid.toAddZeroClass`	—	—
`addMonoidHomCongrLeftEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `addMonoidHomCongrLeftEquiv` `AddMonoidHom.comp` `toAddMonoidHom`	—	—
`addMonoidHomCongrLeftEquiv_trans` 📖	mathematical	—	`addMonoidHomCongrLeftEquiv` `trans` `AddZero.toAdd` `AddZeroClass.toAddZero` `Equiv.trans` `AddMonoidHom` `AddMonoid.toAddZeroClass`	—	—
`addMonoidHomCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `EquivLike.toFunLike` `instEquivLike` `addMonoidHomCongrLeft` `AddMonoidHom.comp` `AddMonoidHomClass.toAddMonoidHom` `AddZero.toAdd` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass` `symm`	—	—
`addMonoidHomCongrLeft_refl` 📖	mathematical	—	`addMonoidHomCongrLeft` `refl` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add`	—	—
`addMonoidHomCongrLeft_trans` 📖	mathematical	—	`addMonoidHomCongrLeft` `trans` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add`	—	—
`addMonoidHomCongrRightEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `addMonoidHomCongrRightEquiv` `AddMonoidHom.comp` `toAddMonoidHom`	—	—
`addMonoidHomCongrRightEquiv_refl` 📖	mathematical	—	`addMonoidHomCongrRightEquiv` `refl` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Equiv.refl` `AddMonoidHom`	—	—
`addMonoidHomCongrRightEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `addMonoidHomCongrRightEquiv` `AddMonoidHom.comp` `toAddMonoidHom` `symm` `AddZero.toAdd`	—	—
`addMonoidHomCongrRightEquiv_trans` 📖	mathematical	—	`addMonoidHomCongrRightEquiv` `trans` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Equiv.trans` `AddMonoidHom`	—	—
`addMonoidHomCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `EquivLike.toFunLike` `instEquivLike` `addMonoidHomCongrRight` `AddMonoidHom.comp` `AddMonoidHomClass.toAddMonoidHom` `AddZero.toAdd` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass`	—	—
`addMonoidHomCongrRight_refl` 📖	mathematical	—	`addMonoidHomCongrRight` `refl` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddMonoidHom.add`	—	—
`addMonoidHomCongrRight_trans` 📖	mathematical	—	`addMonoidHomCongrRight` `trans` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddMonoidHom.add`	—	—
`arrowCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Pi.instAdd` `EquivLike.toFunLike` `instEquivLike` `arrowCongr` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	—
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Pi.instAdd` `EquivLike.toFunLike` `instEquivLike` `funUnique` `Unique.instInhabited`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Pi.instAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `funUnique`	—	—
`piCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Pi.instAdd` `EquivLike.toFunLike` `instEquivLike` `piCongrRight`	—	—
`piCongrRight_refl` 📖	mathematical	—	`piCongrRight` `refl` `Pi.instAdd`	—	—
`piCongrRight_symm` 📖	mathematical	—	`symm` `Pi.instAdd` `piCongrRight`	—	—
`piCongrRight_trans` 📖	mathematical	—	`trans` `Pi.instAdd` `piCongrRight`	—	—
`piUnique_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Unique.instInhabited` `Pi.instAdd` `EquivLike.toFunLike` `instEquivLike` `piUnique`	—	—
`piUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Unique.instInhabited` `Pi.instAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `piUnique` `uniqueElim`	—	—
`symm_addMonoidHomCongrLeft` 📖	mathematical	—	`symm` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `addMonoidHomCongrLeft` `AddZero.toAdd`	—	—
`symm_addMonoidHomCongrLeftEquiv` 📖	mathematical	—	`Equiv.symm` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `addMonoidHomCongrLeftEquiv` `symm` `AddZero.toAdd`	—	—
`symm_addMonoidHomCongrRight` 📖	mathematical	—	`symm` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `addMonoidHomCongrRight` `AddZero.toAdd`	—	—
`symm_addMonoidHomCongrRightEquiv` 📖	mathematical	—	`Equiv.symm` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `addMonoidHomCongrRightEquiv` `symm` `AddZero.toAdd`	—	—

AddEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDedekindFiniteAddMonoid_iff` 📖	mathematical	—	`IsDedekindFiniteAddMonoid`	—	`AddEquiv.injective` `Equiv.right_inv` `map_zero` `map_add` `AddEquiv.instAddEquivClass` `IsDedekindFiniteAddMonoid.of_injective` `AddMonoidHom.instAddMonoidHomClass` `EquivLike.injective`
`toAddEquiv_injective` 📖	mathematical	—	`AddEquiv` `toAddEquiv`	—	`DFunLike.ext`

Equiv

Definitions

Name	Category	Theorems
`inv` 📖	CompOp	6 math math: `comap_inv_leftUniformSpace`, `divLeft_eq_inv_trans_mulLeft`, `inv_symm`, `IsometryEquiv.inv_toEquiv`, `inv_apply`, `MeasurableEquiv.inv_toEquiv`
`neg` 📖	CompOp	11 math math: `IsometryEquiv.neg_toEquiv`, `MeasurableEquiv.neg_toEquiv`, `comap_neg_leftUniformSpace`, `Int.divisorsAntidiag_natCast`, `neg_apply`, `neg_symm`, `Int.divisorsAntidiag_neg`, `Int.divisorsAntidiag_ofNat`, `subLeft_eq_neg_trans_addLeft`, `Int.divisorsAntidiag_neg_natCast`, `Int.map_neg_divisorsAntidiag`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `inv` `InvolutiveInv.toInv`	—	—
`inv_symm` 📖	mathematical	—	`symm` `inv`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `neg` `InvolutiveNeg.toNeg`	—	—
`neg_symm` 📖	mathematical	—	`symm` `neg`	—	—

MulEquiv

Definitions

Name	Category	Theorems
`arrowCongr` 📖	CompOp	1 math math: `arrowCongr_apply`
`funUnique` 📖	CompOp	2 math math: `funUnique_symm_apply`, `funUnique_apply`
`instUnique` 📖	CompOp	—
`monoidHomCongrLeft` 📖	CompOp	4 math math: `monoidHomCongrLeft_apply`, `monoidHomCongrLeft_trans`, `monoidHomCongrLeft_refl`, `symm_monoidHomCongrLeft`
`monoidHomCongrLeftEquiv` 📖	CompOp	5 math math: `monoidHomCongrLeftEquiv_refl`, `monoidHomCongrLeftEquiv_apply`, `symm_monoidHomCongrLeftEquiv`, `monoidHomCongrLeftEquiv_trans`, `monoidHomCongrLeftEquiv_symm_apply`
`monoidHomCongrRight` 📖	CompOp	4 math math: `monoidHomCongrRight_refl`, `symm_monoidHomCongrRight`, `monoidHomCongrRight_trans`, `monoidHomCongrRight_apply`
`monoidHomCongrRightEquiv` 📖	CompOp	5 math math: `symm_monoidHomCongrRightEquiv`, `monoidHomCongrRightEquiv_apply`, `monoidHomCongrRightEquiv_trans`, `monoidHomCongrRightEquiv_symm_apply`, `monoidHomCongrRightEquiv_refl`
`ofUnique` 📖	CompOp	—
`piCongrRight` 📖	CompOp	4 math math: `piCongrRight_refl`, `piCongrRight_symm`, `piCongrRight_trans`, `piCongrRight_apply`
`piUnique` 📖	CompOp	2 math math: `piUnique_apply`, `piUnique_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowCongr_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Pi.instMul` `EquivLike.toFunLike` `instEquivLike` `arrowCongr` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	—
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Pi.instMul` `EquivLike.toFunLike` `instEquivLike` `funUnique` `Unique.instInhabited`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Pi.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `funUnique`	—	—
`monoidHomCongrLeftEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `monoidHomCongrLeftEquiv` `MonoidHom.comp` `toMonoidHom` `symm` `MulOne.toMul`	—	—
`monoidHomCongrLeftEquiv_refl` 📖	mathematical	—	`monoidHomCongrLeftEquiv` `refl` `MulOne.toMul` `MulOneClass.toMulOne` `Equiv.refl` `MonoidHom` `Monoid.toMulOneClass`	—	—
`monoidHomCongrLeftEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `monoidHomCongrLeftEquiv` `MonoidHom.comp` `toMonoidHom`	—	—
`monoidHomCongrLeftEquiv_trans` 📖	mathematical	—	`monoidHomCongrLeftEquiv` `trans` `MulOne.toMul` `MulOneClass.toMulOne` `Equiv.trans` `MonoidHom` `Monoid.toMulOneClass`	—	—
`monoidHomCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul` `EquivLike.toFunLike` `instEquivLike` `monoidHomCongrLeft` `MonoidHom.comp` `MonoidHomClass.toMonoidHom` `MulOne.toMul` `MulEquivClass.instMonoidHomClass` `instMulEquivClass` `symm`	—	—
`monoidHomCongrLeft_refl` 📖	mathematical	—	`monoidHomCongrLeft` `refl` `MulOne.toMul` `MulOneClass.toMulOne` `MonoidHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul`	—	—
`monoidHomCongrLeft_trans` 📖	mathematical	—	`monoidHomCongrLeft` `trans` `MulOne.toMul` `MulOneClass.toMulOne` `MonoidHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul`	—	—
`monoidHomCongrRightEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `monoidHomCongrRightEquiv` `MonoidHom.comp` `toMonoidHom`	—	—
`monoidHomCongrRightEquiv_refl` 📖	mathematical	—	`monoidHomCongrRightEquiv` `refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Equiv.refl` `MonoidHom`	—	—
`monoidHomCongrRightEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `monoidHomCongrRightEquiv` `MonoidHom.comp` `toMonoidHom` `symm` `MulOne.toMul`	—	—
`monoidHomCongrRightEquiv_trans` 📖	mathematical	—	`monoidHomCongrRightEquiv` `trans` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Equiv.trans` `MonoidHom`	—	—
`monoidHomCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul` `EquivLike.toFunLike` `instEquivLike` `monoidHomCongrRight` `MonoidHom.comp` `MonoidHomClass.toMonoidHom` `MulOne.toMul` `MulEquivClass.instMonoidHomClass` `instMulEquivClass`	—	—
`monoidHomCongrRight_refl` 📖	mathematical	—	`monoidHomCongrRight` `refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MonoidHom.mul`	—	—
`monoidHomCongrRight_trans` 📖	mathematical	—	`monoidHomCongrRight` `trans` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MonoidHom.mul`	—	—
`piCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Pi.instMul` `EquivLike.toFunLike` `instEquivLike` `piCongrRight`	—	—
`piCongrRight_refl` 📖	mathematical	—	`piCongrRight` `refl` `Pi.instMul`	—	—
`piCongrRight_symm` 📖	mathematical	—	`symm` `Pi.instMul` `piCongrRight`	—	—
`piCongrRight_trans` 📖	mathematical	—	`trans` `Pi.instMul` `piCongrRight`	—	—
`piUnique_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Unique.instInhabited` `Pi.instMul` `EquivLike.toFunLike` `instEquivLike` `piUnique`	—	—
`piUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Unique.instInhabited` `Pi.instMul` `EquivLike.toFunLike` `instEquivLike` `symm` `piUnique` `uniqueElim`	—	—
`symm_monoidHomCongrLeft` 📖	mathematical	—	`symm` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul` `monoidHomCongrLeft` `MulOne.toMul`	—	—
`symm_monoidHomCongrLeftEquiv` 📖	mathematical	—	`Equiv.symm` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `monoidHomCongrLeftEquiv` `symm` `MulOne.toMul`	—	—
`symm_monoidHomCongrRight` 📖	mathematical	—	`symm` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul` `monoidHomCongrRight` `MulOne.toMul`	—	—
`symm_monoidHomCongrRightEquiv` 📖	mathematical	—	`Equiv.symm` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `monoidHomCongrRightEquiv` `symm` `MulOne.toMul`	—	—

MulEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDedekindFiniteMonoid_iff` 📖	mathematical	—	`IsDedekindFiniteMonoid`	—	`MulEquiv.injective` `Equiv.right_inv` `map_one` `map_mul` `MulEquiv.instMulEquivClass` `IsDedekindFiniteMonoid.of_injective` `MonoidHom.instMonoidHomClass` `EquivLike.injective`
`toMulEquiv_injective` 📖	mathematical	—	`MulEquiv` `toMulEquiv`	—	`DFunLike.ext`

---

← Back to Index