TransferInstance

📁 Source: Mathlib/Algebra/Group/TransferInstance.lean

Statistics

Metric	Count
Definitions `Neg`, `add`, `addCommGroup`, `addCommMonoid`, `addCommSemigroup`, `addEquiv`, `addGroup`, `addMonoid`, `addSemigroup`, `addZeroClass`, `commGroup`, `commMonoid`, `commSemigroup`, `div`, `group`, `monoid`, `mul`, `mulEquiv`, `mulOneClass`, `one`, `pow`, `semigroup`, `smul`, `sub`, `vadd`, `zero`	26
Theorems `addEquiv_apply`, `addEquiv_symm_apply`, `add_def`, `div_def`, `inv_def`, `isCancelAdd`, `isCancelMul`, `isLeftCancelAdd`, `isLeftCancelMul`, `isRightCancelAdd`, `isRightCancelMul`, `mulEquiv_apply`, `mulEquiv_symm_apply`, `mul_def`, `neg_def`, `one_def`, `pow_def`, `smul_def`, `sub_def`, `vadd_def`, `zero_def`, `exists_type_univ_nonempty_addEquiv`, `exists_type_univ_nonempty_mulEquiv`	23
Total	49

Equiv

Definitions

Name	Category	Theorems
`Neg` 📖	CompOp	1 math math: `neg_def`
`add` 📖	CompOp	8 math math: `add_def`, `addEquiv_apply`, `isCancelAdd`, `isLeftCancelAdd`, `ringEquiv_apply`, `addEquiv_symm_apply`, `ringEquiv_symm_apply`, `isRightCancelAdd`
`addCommGroup` 📖	CompOp	—
`addCommMonoid` 📖	CompOp	5 math math: `coalgebraIsCocomm`, `tensorProductAssoc_def`, `toLinearEquiv_continuousLinearEquiv`, `tensorProductComm_def`, `moduleIsTorsionFree`
`addCommSemigroup` 📖	CompOp	—
`addEquiv` 📖	CompOp	2 math math: `addEquiv_apply`, `addEquiv_symm_apply`
`addGroup` 📖	CompOp	—
`addMonoid` 📖	CompOp	—
`addSemigroup` 📖	CompOp	—
`addZeroClass` 📖	CompOp	—
`commGroup` 📖	CompOp	—
`commMonoid` 📖	CompOp	—
`commSemigroup` 📖	CompOp	—
`div` 📖	CompOp	1 math math: `div_def`
`group` 📖	CompOp	—
`monoid` 📖	CompOp	—
`mul` 📖	CompOp	8 math math: `isCancelMul`, `mulEquiv_apply`, `isRightCancelMul`, `mul_def`, `ringEquiv_apply`, `mulEquiv_symm_apply`, `ringEquiv_symm_apply`, `isLeftCancelMul`
`mulEquiv` 📖	CompOp	2 math math: `mulEquiv_apply`, `mulEquiv_symm_apply`
`mulOneClass` 📖	CompOp	—
`one` 📖	CompOp	1 math math: `one_def`
`pow` 📖	CompOp	1 math math: `pow_def`
`semigroup` 📖	CompOp	—
`smul` 📖	CompOp	6 math math: `faithfulSMul`, `isCentralScalar`, `smul_def`, `isScalarTower`, `noZeroSMulDivisors`, `smulCommClass`
`sub` 📖	CompOp	1 math math: `sub_def`
`vadd` 📖	CompOp	5 math math: `faithfulVAdd`, `vaddAssocClass`, `vaddCommClass`, `vadd_def`, `isCentralVAdd`
`zero` 📖	CompOp	2 math math: `zero_def`, `noZeroSMulDivisors`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquiv` `Equiv` `instEquivLike`	—	—
`addEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv` `Equiv` `instEquivLike` `symm`	—	—
`add_def` 📖	mathematical	—	`add` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`div_def` 📖	mathematical	—	`div` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`inv_def` 📖	mathematical	—	`Inv` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`isCancelAdd` 📖	mathematical	—	`IsCancelAdd` `add`	—	`Function.Injective.isCancelAdd` `injective` `apply_symm_apply`
`isCancelMul` 📖	mathematical	—	`IsCancelMul` `mul`	—	`Function.Injective.isCancelMul` `injective` `apply_symm_apply`
`isLeftCancelAdd` 📖	mathematical	—	`IsLeftCancelAdd` `add`	—	`Function.Injective.isLeftCancelAdd` `injective` `apply_symm_apply`
`isLeftCancelMul` 📖	mathematical	—	`IsLeftCancelMul` `mul`	—	`Function.Injective.isLeftCancelMul` `injective` `apply_symm_apply`
`isRightCancelAdd` 📖	mathematical	—	`IsRightCancelAdd` `add`	—	`Function.Injective.isRightCancelAdd` `injective` `apply_symm_apply`
`isRightCancelMul` 📖	mathematical	—	`IsRightCancelMul` `mul`	—	`Function.Injective.isRightCancelMul` `injective` `apply_symm_apply`
`mulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquiv` `Equiv` `instEquivLike`	—	—
`mulEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulEquiv` `Equiv` `instEquivLike` `symm`	—	—
`mul_def` 📖	mathematical	—	`mul` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`neg_def` 📖	mathematical	—	`Neg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`one_def` 📖	mathematical	—	`one` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`pow_def` 📖	mathematical	—	`pow` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`smul_def` 📖	mathematical	—	`smul` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`sub_def` 📖	mathematical	—	`sub` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `vadd` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`zero_def` 📖	mathematical	—	`zero` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_type_univ_nonempty_addEquiv` 📖	mathematical	—	`AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`exists_equiv_fin`
`exists_type_univ_nonempty_mulEquiv` 📖	mathematical	—	`MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`exists_equiv_fin`

---

← Back to Index