Equiv

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

Statistics

Metric	Count
Definitions `neg`, `addLeft`, `addRight`, `addLeft`, `addRight`, `divLeft`, `divRight`, `mulLeft`, `mulRight`, `subLeft`, `subRight`, `inv`, `mapEquiv`, `mulLeft`, `mulRight`, `toAddUnits`, `toUnits`, `unitsEquivProdSubtype`	18
Theorems `isAddUnit_map`, `neg_apply`, `neg_symm`, `addLeft_bijective`, `addRight_bijective`, `addLeft_apply`, `addLeft_bijective`, `addLeft_symm`, `addRight_apply`, `addRight_bijective`, `addRight_symm`, `addLeft_symm`, `addLeft_symm_apply`, `addRight_symm`, `addRight_symm_apply`, `coe_addLeft`, `coe_addRight`, `coe_mulLeft`, `coe_mulRight`, `divLeft_apply`, `divLeft_eq_inv_trans_mulLeft`, `divLeft_involutive`, `divLeft_symm_apply`, `divRight_apply`, `divRight_eq_mulRight_inv`, `divRight_symm_apply`, `mulLeft_symm`, `mulLeft_symm_apply`, `mulRight_symm`, `mulRight_symm_apply`, `subLeft_apply`, `subLeft_eq_neg_trans_addLeft`, `subLeft_involutive`, `subLeft_symm_apply`, `subRight_apply`, `subRight_eq_addRight_neg`, `subRight_symm_apply`, `symm_divLeft`, `symm_subLeft`, `mulLeft_bijective`, `mulRight_bijective`, `inv_apply`, `inv_symm`, `isUnit_map`, `coe_mapEquiv`, `mapEquiv_symm`, `mulLeft_apply`, `mulLeft_bijective`, `mulLeft_symm`, `mulRight_apply`, `mulRight_bijective`, `mulRight_symm`, `isLocalHom_equiv`, `toAddUnits_symm_apply`, `toAddUnits_val_apply`, `toUnits_symm_apply`, `toUnits_val_apply`, `unitsEquivProdSubtype_apply_coe`, `val_inv_unitsEquivProdSubtype_symm_apply`, `val_toAddUnits_apply`, `val_toUnits_apply`, `val_unitsEquivProdSubtype_symm_apply`	62
Total	80

AddEquiv

Definitions

Name	Category	Theorems
`neg` 📖	CompOp	4 math math: `neg_apply`, `neg_symm`, `Int.univ_addEquiv`, `Int.addEquiv_eq_refl_or_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddUnit_map` 📖	mathematical	—	`IsAddUnit` `DFunLike.coe` `EquivLike.toFunLike`	—	`EquivLike.injective` `EquivLike.apply_inv_apply` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `EquivLike.inv_apply_apply` `IsAddUnit.map` `AddMonoidHom.instAddMonoidHomClass`
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `EquivLike.toFunLike` `instEquivLike` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	—
`neg_symm` 📖	mathematical	—	`symm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `neg`	—	—

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft_bijective` 📖	mathematical	—	`Function.Bijective` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`Equiv.bijective`
`addRight_bijective` 📖	mathematical	—	`Function.Bijective` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`Equiv.bijective`

AddUnits

Definitions

Name	Category	Theorems
`addLeft` 📖	CompOp	2 math math: `addLeft_symm`, `addLeft_apply`
`addRight` 📖	CompOp	2 math math: `addRight_apply`, `addRight_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `addLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `val`	—	—
`addLeft_bijective` 📖	mathematical	—	`Function.Bijective` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `val`	—	`Equiv.bijective`
`addLeft_symm` 📖	mathematical	—	`Equiv.symm` `addLeft` `AddUnits` `instNeg`	—	`Equiv.ext`
`addRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `addRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `val`	—	—
`addRight_bijective` 📖	mathematical	—	`Function.Bijective` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `val`	—	`Equiv.bijective`
`addRight_symm` 📖	mathematical	—	`Equiv.symm` `addRight` `AddUnits` `instNeg`	—	`Equiv.ext`

Equiv

Definitions

Name	Category	Theorems
`addLeft` 📖	CompOp	13 math math: `zsmul_addLeft`, `Int.addLeft_one_isCycle`, `neg_addLeft`, `nsmul_addLeft`, `MeasurableEquiv.toEquiv_addLeft`, `addLeft_add`, `coe_addLeft`, `OrderIso.addLeft_toEquiv`, `addLeft_symm_apply`, `addLeft_zero`, `subLeft_eq_neg_trans_addLeft`, `addLeft_symm`, `IsometryEquiv.addLeft_toEquiv`
`addRight` 📖	CompOp	13 math math: `addRight_add`, `MeasurableEquiv.toEquiv_addRight`, `addRight_symm_apply`, `neg_addRight`, `addRight_zero`, `coe_addRight`, `nsmul_addRight`, `OrderIso.addRight_toEquiv`, `Int.addRight_one_isCycle`, `zsmul_addRight`, `addRight_symm`, `IsometryEquiv.addRight_toEquiv`, `subRight_eq_addRight_neg`
`divLeft` 📖	CompOp	6 math math: `divLeft_involutive`, `divLeft_symm_apply`, `divLeft_eq_inv_trans_mulLeft`, `IsometryEquiv.divLeft_toEquiv`, `divLeft_apply`, `symm_divLeft`
`divRight` 📖	CompOp	4 math math: `divRight_symm_apply`, `divRight_apply`, `divRight_eq_mulRight_inv`, `IsometryEquiv.divRight_toEquiv`
`mulLeft` 📖	CompOp	12 math math: `MeasurableEquiv.toEquiv_mulLeft`, `divLeft_eq_inv_trans_mulLeft`, `pow_mulLeft`, `mulLeft_one`, `zpow_mulLeft`, `coe_mulLeft`, `mulLeft_symm_apply`, `mulLeft_symm`, `OrderIso.mulLeft_toEquiv`, `mulLeft_mul`, `IsometryEquiv.mulLeft_toEquiv`, `inv_mulLeft`
`mulRight` 📖	CompOp	12 math math: `MeasurableEquiv.toEquiv_mulRight`, `zpow_mulRight`, `OrderIso.mulRight_toEquiv`, `IsometryEquiv.mulRight_toEquiv`, `inv_mulRight`, `mulRight_symm`, `coe_mulRight`, `mulRight_mul`, `divRight_eq_mulRight_inv`, `mulRight_symm_apply`, `mulRight_one`, `pow_mulRight`
`subLeft` 📖	CompOp	7 math math: `symm_subLeft`, `IsometryEquiv.subLeft_toEquiv`, `subLeft_symm_apply`, `subLeft_apply`, `pointReflection_eq_subLeft`, `subLeft_eq_neg_trans_addLeft`, `subLeft_involutive`
`subRight` 📖	CompOp	4 math math: `subRight_apply`, `IsometryEquiv.subRight_toEquiv`, `subRight_eq_addRight_neg`, `subRight_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft_symm` 📖	mathematical	—	`symm` `addLeft` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext`
`addLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `addLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`addRight_symm` 📖	mathematical	—	`symm` `addRight` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext`
`addRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `addRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`coe_addLeft` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `addLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`coe_addRight` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `addRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`coe_mulLeft` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`coe_mulRight` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`divLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `divLeft` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`divLeft_eq_inv_trans_mulLeft` 📖	mathematical	—	`divLeft` `trans` `inv` `DivisionMonoid.toInvolutiveInv` `Group.toDivisionMonoid` `mulLeft`	—	`ext` `div_eq_mul_inv`
`divLeft_involutive` 📖	mathematical	—	`Function.Involutive` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `divLeft` `CommGroup.toGroup`	—	`div_div_cancel`
`divLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `divLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`divRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `divRight` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`divRight_eq_mulRight_inv` 📖	mathematical	—	`divRight` `mulRight` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext` `div_eq_mul_inv`
`divRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `divRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mulLeft_symm` 📖	mathematical	—	`symm` `mulLeft` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext`
`mulLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`mulRight_symm` 📖	mathematical	—	`symm` `mulRight` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext`
`mulRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`subLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `subLeft` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`subLeft_eq_neg_trans_addLeft` 📖	mathematical	—	`subLeft` `trans` `neg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid` `addLeft`	—	`ext` `sub_eq_add_neg`
`subLeft_involutive` 📖	mathematical	—	`Function.Involutive` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `subLeft` `AddCommGroup.toAddGroup`	—	`sub_sub_cancel`
`subLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `subLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`subRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `subRight` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`subRight_eq_addRight_neg` 📖	mathematical	—	`subRight` `addRight` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext` `sub_eq_add_neg`
`subRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `subRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`symm_divLeft` 📖	mathematical	—	`symm` `divLeft` `CommGroup.toGroup`	—	`ext` `inv_mul_eq_div`
`symm_subLeft` 📖	mathematical	—	`symm` `subLeft` `AddCommGroup.toAddGroup`	—	`ext` `neg_add_eq_sub`

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_bijective` 📖	mathematical	—	`Function.Bijective` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`Equiv.bijective`
`mulRight_bijective` 📖	mathematical	—	`Function.Bijective` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`Equiv.bijective`

MulEquiv

Definitions

Name	Category	Theorems
`inv` 📖	CompOp	2 math math: `inv_symm`, `inv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `EquivLike.toFunLike` `instEquivLike` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	—
`inv_symm` 📖	mathematical	—	`symm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `inv`	—	—
`isUnit_map` 📖	mathematical	—	`IsUnit` `DFunLike.coe` `EquivLike.toFunLike`	—	`EquivLike.injective` `EquivLike.apply_inv_apply` `map_one` `MonoidHomClass.toOneHomClass` `MulEquivClass.instMonoidHomClass` `map_mul` `MonoidHomClass.toMulHomClass` `EquivLike.inv_apply_apply` `IsUnit.map` `MonoidHom.instMonoidHomClass`

Units

Definitions

Name	Category	Theorems
`mapEquiv` 📖	CompOp	4 math math: `mapEquiv_symm`, `toMulEquiv_mapContinuousMulEquiv`, `coe_mapEquiv`, `ClassGroup.equiv_mk`
`mulLeft` 📖	CompOp	3 math math: `ENNReal.mulLeftOrderIso_toEquiv`, `mulLeft_symm`, `mulLeft_apply`
`mulRight` 📖	CompOp	3 math math: `ENNReal.mulRightOrderIso_toEquiv`, `mulRight_symm`, `mulRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mapEquiv` 📖	mathematical	—	`val` `DFunLike.coe` `MulEquiv` `Units` `instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mapEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`mapEquiv_symm` 📖	mathematical	—	`MulEquiv.symm` `Units` `instMul` `mapEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	—
`mulLeft_bijective` 📖	mathematical	—	`Function.Bijective` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`Equiv.bijective`
`mulLeft_symm` 📖	mathematical	—	`Equiv.symm` `mulLeft` `Units` `instInv`	—	`Equiv.ext`
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	—
`mulRight_bijective` 📖	mathematical	—	`Function.Bijective` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`Equiv.bijective`
`mulRight_symm` 📖	mathematical	—	`Equiv.symm` `mulRight` `Units` `instInv`	—	`Equiv.ext`

(root)

Definitions

Name	Category	Theorems
`toAddUnits` 📖	CompOp	5 math math: `val_toAddUnits_apply`, `AddSubgroup.mem_iff_toAddUnits_mem_addUnits`, `AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem`, `toAddUnits_symm_apply`, `toAddUnits_val_apply`
`toUnits` 📖	CompOp	5 math math: `val_toUnits_apply`, `Subgroup.mem_ofUnits_iff_toUnits_mem`, `toUnits_symm_apply`, `toUnits_val_apply`, `Subgroup.mem_iff_toUnits_mem_units`
`unitsEquivProdSubtype` 📖	CompOp	3 math math: `val_inv_unitsEquivProdSubtype_symm_apply`, `unitsEquivProdSubtype_apply_coe`, `val_unitsEquivProdSubtype_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHom_equiv` 📖	mathematical	—	`IsLocalHom` `EquivLike.toFunLike`	—	—
`toAddUnits_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddUnits` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddUnits.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `toAddUnits` `AddUnits.val`	—	—
`toAddUnits_val_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddUnits` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toAddUnits` `AddUnits.val`	—	`AddEquiv.apply_eq_iff_symm_apply`
`toUnits_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Units` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `toUnits` `Units.val`	—	—
`toUnits_val_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Units` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toUnits` `Units.val`	—	—
`unitsEquivProdSubtype_apply_coe` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `DFunLike.coe` `Equiv` `Units` `EquivLike.toFunLike` `Equiv.instEquivLike` `unitsEquivProdSubtype` `Units.val` `Units.instInv`	—	—
`val_inv_unitsEquivProdSubtype_symm_apply` 📖	mathematical	—	`Units.val` `Units` `Units.instInv` `DFunLike.coe` `Equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `unitsEquivProdSubtype`	—	—
`val_toAddUnits_apply` 📖	mathematical	—	`AddUnits.val` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `AddEquiv` `AddUnits` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toAddUnits`	—	—
`val_toUnits_apply` 📖	mathematical	—	`Units.val` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `MulEquiv` `Units` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toUnits`	—	—
`val_unitsEquivProdSubtype_symm_apply` 📖	mathematical	—	`Units.val` `DFunLike.coe` `Equiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `Units` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `unitsEquivProdSubtype`	—	—

---

← Back to Index