Shrink

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

Statistics

Metric	Count
Definitions `addEquiv`, `instAdd`, `instAddAction`, `instAddCommGroup`, `instAddCommMonoid`, `instAddCommSemigroup`, `instAddGroup`, `instAddMonoid`, `instAddSemigroup`, `instAddZeroClass`, `instCommGroup`, `instCommMonoid`, `instCommSemigroup`, `instDiv`, `instGroup`, `instInv`, `instMonoid`, `instMul`, `instMulAction`, `instMulOneClass`, `instNSMul`, `instNeg`, `instOne`, `instPow`, `instSemigroup`, `instSub`, `instZero`, `mulEquiv`	28
Theorems `instIsCancelAdd`, `instIsCancelMul`, `instIsLeftCancelAdd`, `instIsLeftCancelMul`, `instIsRightCancelAdd`, `instIsRightCancelMul`, `equivShrink_add`, `equivShrink_div`, `equivShrink_inv`, `equivShrink_mul`, `equivShrink_neg`, `equivShrink_smul`, `equivShrink_sub`, `equivShrink_symm_add`, `equivShrink_symm_div`, `equivShrink_symm_inv`, `equivShrink_symm_mul`, `equivShrink_symm_neg`, `equivShrink_symm_one`, `equivShrink_symm_smul`, `equivShrink_symm_sub`, `equivShrink_symm_zero`	22
Total	50

Shrink

Definitions

Name	Category	Theorems
`addEquiv` 📖	CompOp	2 math math: `AddCommGrpCat.Colimits.colimitCocone_ι_app`, `AddCommGrpCat.Colimits.Quot.desc_colimitCocone`
`instAdd` 📖	CompOp	7 math math: `instIsRightCancelAdd`, `AddCommGrpCat.Colimits.colimitCocone_ι_app`, `instIsLeftCancelAdd`, `AddCommGrpCat.Colimits.Quot.desc_colimitCocone`, `equivShrink_add`, `equivShrink_symm_add`, `instIsCancelAdd`
`instAddAction` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	3 math math: `AddCommGrpCat.Colimits.colimitCocone_ι_app`, `AddCommGrpCat.Colimits.colimitCocone_pt`, `ModuleCat.isSeparator`
`instAddCommMonoid` 📖	CompOp	8 math math: `linearEquiv_symm_apply`, `Module.Free.Module.free_shrink`, `Module.Flat.shrink`, `continuousLinearEquiv_symm_apply`, `continuousLinearEquiv_apply`, `instFreeCarrierX₂ModuleCatProjectiveShortComplex`, `Module.Finite.Module.finite_shrink`, `linearEquiv_apply`
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAddSemigroup` 📖	CompOp	—
`instAddZeroClass` 📖	CompOp	2 math math: `AddCommGrpCat.Colimits.colimitCocone_ι_app`, `AddCommGrpCat.Colimits.Quot.desc_colimitCocone`
`instCommGroup` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instCommSemigroup` 📖	CompOp	—
`instDiv` 📖	CompOp	2 math math: `equivShrink_symm_div`, `equivShrink_div`
`instGroup` 📖	CompOp	—
`instInv` 📖	CompOp	2 math math: `equivShrink_inv`, `equivShrink_symm_inv`
`instMonoid` 📖	CompOp	—
`instMul` 📖	CompOp	5 math math: `instIsRightCancelMul`, `equivShrink_mul`, `instIsCancelMul`, `instIsLeftCancelMul`, `equivShrink_symm_mul`
`instMulAction` 📖	CompOp	—
`instMulOneClass` 📖	CompOp	—
`instNSMul` 📖	CompOp	2 math math: `equivShrink_smul`, `equivShrink_symm_smul`
`instNeg` 📖	CompOp	2 math math: `equivShrink_neg`, `equivShrink_symm_neg`
`instOne` 📖	CompOp	1 math math: `equivShrink_symm_one`
`instPow` 📖	CompOp	—
`instSemigroup` 📖	CompOp	—
`instSub` 📖	CompOp	2 math math: `equivShrink_symm_sub`, `equivShrink_sub`
`instZero` 📖	CompOp	1 math math: `equivShrink_symm_zero`
`mulEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelAdd` 📖	mathematical	—	`IsCancelAdd` `Shrink` `instAdd`	—	`Equiv.isCancelAdd`
`instIsCancelMul` 📖	mathematical	—	`IsCancelMul` `Shrink` `instMul`	—	`Equiv.isCancelMul`
`instIsLeftCancelAdd` 📖	mathematical	—	`IsLeftCancelAdd` `Shrink` `instAdd`	—	`Equiv.isLeftCancelAdd`
`instIsLeftCancelMul` 📖	mathematical	—	`IsLeftCancelMul` `Shrink` `instMul`	—	`Equiv.isLeftCancelMul`
`instIsRightCancelAdd` 📖	mathematical	—	`IsRightCancelAdd` `Shrink` `instAdd`	—	`Equiv.isRightCancelAdd`
`instIsRightCancelMul` 📖	mathematical	—	`IsRightCancelMul` `Shrink` `instMul`	—	`Equiv.isRightCancelMul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivShrink_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instAdd`	—	`Equiv.symm_apply_apply`
`equivShrink_div` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instDiv`	—	`Equiv.symm_apply_apply`
`equivShrink_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instInv`	—	`Equiv.symm_apply_apply`
`equivShrink_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instMul`	—	`Equiv.symm_apply_apply`
`equivShrink_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instNeg`	—	`Equiv.symm_apply_apply`
`equivShrink_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instNSMul`	—	`Equiv.symm_apply_apply`
`equivShrink_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Shrink.instSub`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instAdd`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_div` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instDiv`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instInv`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instMul`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instNeg`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instOne`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instNSMul`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instSub`	—	`Equiv.symm_apply_apply`
`equivShrink_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Shrink.instZero`	—	`Equiv.symm_apply_apply`

---

← Back to Index