Lemmas

📁 Source: Mathlib/Algebra/Group/Pi/Lemmas.lean

Statistics

Metric	Count
Definitions `coeFn`, `compLeft`, `coeFn`, `compLeft`, `single`, `hom`, `hom`, `coeFn`, `compLeft`, `mulSingle`, `coeFn`, `compLeft`, `mulSingle`, `addHom`, `addMonoidHom`, `constAddHom`, `constAddMonoidHom`, `constMonoidHom`, `constMulHom`, `evalAddHom`, `evalAddMonoidHom`, `evalMonoidHom`, `evalMulHom`, `monoidHom`, `mulHom`, `single`	26
Theorems `pi`, `coeFn_apply`, `coe_add`, `compLeft_apply`, `coeFn_apply`, `coe_single`, `compLeft_apply`, `single_apply`, `pi`, `pi`, `hom_apply`, `hom_apply`, `const_eq_one`, `const_eq_zero`, `const_ne_one`, `const_ne_zero`, `update_add`, `update_div`, `update_inv`, `update_mul`, `update_neg`, `update_one`, `update_sub`, `update_zero`, `coeFn_apply`, `coe_mulSingle`, `compLeft_apply`, `mulSingle_apply`, `coeFn_apply`, `coe_mul`, `compLeft_apply`, `coe_mulSingle`, `mulSingle_apply`, `addCommute_iff`, `addHom_apply`, `addHom_injective`, `addMonoidHom_apply`, `addMonoidHom_injective`, `addSemiconjBy_iff`, `coe_evalMonoidHom`, `commute_iff`, `constAddHom_apply`, `constAddMonoidHom_apply`, `constMonoidHom_apply`, `constMulHom_apply`, `evalAddHom_apply`, `evalAddMonoidHom_apply`, `evalMonoidHom_apply`, `evalMulHom_apply`, `instIsAddTorsionFree`, `instIsMulTorsionFree`, `monoidHom_apply`, `monoidHom_injective`, `mulHom_apply`, `mulHom_injective`, `mulSingle_apply_commute`, `mulSingle_commute`, `mulSingle_comp_equiv`, `mulSingle_div`, `mulSingle_inf`, `mulSingle_inv`, `mulSingle_mono`, `mulSingle_mul`, `mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle`, `mulSingle_pow`, `mulSingle_strictMono`, `mulSingle_sup`, `mulSingle_zpow`, `one_anti`, `one_mono`, `semiconjBy_iff`, `single_add`, `single_addCommute`, `single_add_single_eq_single_add_single`, `single_apply_addCommute`, `single_comp_equiv`, `single_inf`, `single_mono`, `single_neg`, `single_nsmul`, `single_strictMono`, `single_sub`, `single_sup`, `single_zsmul`, `update_eq_div_mul_mulSingle`, `update_eq_sub_add_single`, `zero_anti`, `zero_mono`, `pi`, `piecewise_add`, `piecewise_div`, `piecewise_inv`, `piecewise_mul`, `piecewise_neg`, `piecewise_sub`, `preimage_one`, `preimage_zero`, `range_one`, `range_zero`, `curry_add`, `curry_inv`, `curry_mul`, `curry_mulSingle`, `curry_neg`, `curry_one`, `curry_single`, `curry_zero`, `uncurry_add`, `uncurry_inv`, `uncurry_mul`, `uncurry_mulSingle_mulSingle`, `uncurry_neg`, `uncurry_one`, `uncurry_single_single`, `uncurry_zero`, `coe_single`, `single_apply`	117
Total	143

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi` 📖	mathematical	`AddCommute`	`Pi.instAdd`	—	`AddSemiconjBy.pi`

AddHom

Definitions

Name	Category	Theorems
`coeFn` 📖	CompOp	1 math math: `coeFn_apply`
`compLeft` 📖	CompOp	1 math math: `compLeft_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instAdd` `Pi.instAdd` `funLike` `coeFn`	—	—
`coe_add` 📖	mathematical	—	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `DFunLike.coe` `AddHom` `funLike`	—	—
`compLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `Pi.instAdd` `funLike` `compLeft`	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
`coeFn` 📖	CompOp	2 math math: `coe_dfinsuppSumAddHom`, `coeFn_apply`
`compLeft` 📖	CompOp	1 math math: `compLeft_apply`
`single` 📖	CompOp	8 math math: `AddSubmonoid.iSup_map_single`, `AddSubmonoid.pi_le_iff`, `AddSubmonoid.le_comap_single_pi`, `AddSubmonoid.iSup_map_single_le`, `single_apply`, `AddSubgroup.pi_le_iff`, `coe_single`, `functions_ext'_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Pi.addZeroClass` `instFunLike` `coeFn`	—	—
`coe_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `instFunLike` `single` `Pi.single` `AddZero.toZero`	—	—
`compLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `instFunLike` `compLeft`	—	—
`single_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `instFunLike` `single` `Pi.single` `AddZero.toZero`	—	—

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi` 📖	mathematical	`AddSemiconjBy`	`Pi.instAdd`	—	—

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi` 📖	mathematical	`Commute`	`Pi.instMul`	—	`SemiconjBy.pi`

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_eq_one` 📖	mathematical	—	`Pi.instOne`	—	—
`const_eq_zero` 📖	mathematical	—	`Pi.instZero`	—	—
`const_ne_one` 📖	—	—	—	—	`Iff.not` `const_eq_one`
`const_ne_zero` 📖	—	—	—	—	`Iff.not` `const_eq_zero`
`update_add` 📖	mathematical	—	`update` `Pi.instAdd`	—	`apply_update₂`
`update_div` 📖	mathematical	—	`update` `Pi.instDiv`	—	`apply_update₂`
`update_inv` 📖	mathematical	—	`update` `Pi.instInv`	—	`apply_update`
`update_mul` 📖	mathematical	—	`update` `Pi.instMul`	—	`apply_update₂`
`update_neg` 📖	mathematical	—	`update` `Pi.instNeg`	—	`apply_update`
`update_one` 📖	mathematical	—	`update` `Pi.instOne`	—	`update_eq_self`
`update_sub` 📖	mathematical	—	`update` `Pi.instSub`	—	`apply_update₂`
`update_zero` 📖	mathematical	—	`update` `Pi.instZero`	—	`update_eq_self`

Function.ExtendByOne

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	1 math math: `hom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `MonoidHom.instFunLike` `hom` `Function.extend` `Pi.instOne` `MulOne.toOne`	—	—

Function.ExtendByZero

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	1 math math: `hom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `hom` `Function.extend` `Pi.instZero` `AddZero.toZero`	—	—

MonoidHom

Definitions

Name	Category	Theorems
`coeFn` 📖	CompOp	1 math math: `coeFn_apply`
`compLeft` 📖	CompOp	1 math math: `compLeft_apply`
`mulSingle` 📖	CompOp	9 math math: `functions_ext'_iff`, `Subgroup.pi_le_iff`, `Submonoid.iSup_map_mulSingle_le`, `Submonoid.iSup_map_mulSingle`, `Submonoid.pi_le_iff`, `Submonoid.le_comap_mulSingle_pi`, `PiTensorProduct.singleAlgHom_apply`, `mulSingle_apply`, `coe_mulSingle`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instCommMonoid` `Pi.mulOneClass` `instFunLike` `coeFn`	—	—
`coe_mulSingle` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `instFunLike` `mulSingle` `Pi.mulSingle` `MulOne.toOne`	—	—
`compLeft_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `instFunLike` `compLeft`	—	—
`mulSingle_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `instFunLike` `mulSingle` `Pi.mulSingle` `MulOne.toOne`	—	—

MulHom

Definitions

Name	Category	Theorems
`coeFn` 📖	CompOp	1 math math: `coeFn_apply`
`compLeft` 📖	CompOp	1 math math: `compLeft_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `CommMagma.toMul` `CommSemigroup.toCommMagma` `instMul` `Pi.instMul` `funLike` `coeFn`	—	—
`coe_mul` 📖	mathematical	—	`Pi.instMul` `CommMagma.toMul` `CommSemigroup.toCommMagma` `DFunLike.coe` `MulHom` `funLike`	—	—
`compLeft_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `Pi.instMul` `funLike` `compLeft`	—	—

OneHom

Definitions

Name	Category	Theorems
`mulSingle` 📖	CompOp	2 math math: `coe_mulSingle`, `mulSingle_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mulSingle` 📖	mathematical	—	`DFunLike.coe` `OneHom` `Pi.instOne` `funLike` `mulSingle` `Pi.mulSingle`	—	—
`mulSingle_apply` 📖	mathematical	—	`DFunLike.coe` `OneHom` `Pi.instOne` `funLike` `mulSingle` `Pi.mulSingle`	—	—

Pi

Definitions

Name	Category	Theorems
`addHom` 📖	CompOp	2 math math: `addHom_apply`, `addHom_injective`
`addMonoidHom` 📖	CompOp	6 math math: `AddCommMonCat.coyonedaType_obj_map`, `AddCommMonCat.coyonedaType_map_app`, `AddCommGrpCat.coyonedaType_obj_map`, `addMonoidHom_apply`, `addMonoidHom_injective`, `AddCommGrpCat.coyonedaType_map_app`
`constAddHom` 📖	CompOp	1 math math: `constAddHom_apply`
`constAddMonoidHom` 📖	CompOp	1 math math: `constAddMonoidHom_apply`
`constMonoidHom` 📖	CompOp	1 math math: `constMonoidHom_apply`
`constMulHom` 📖	CompOp	1 math math: `constMulHom_apply`
`evalAddHom` 📖	CompOp	2 math math: `Matrix.entryAddHom_eq_comp`, `evalAddHom_apply`
`evalAddMonoidHom` 📖	CompOp	13 math math: `LinearMap.toAddMonoidHom_proj`, `AddCommMonCat.coyonedaType_obj_map`, `AddCommMonCat.coyonedaType_map_app`, `Matrix.entryAddMonoidHom_eq_comp`, `AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift`, `AddSubmonoid.le_pi_iff`, `Matrix.evalAddMonoidHom_comp_diagAddMonoidHom`, `AddCommGrpCat.coyonedaType_obj_map`, `AddCommGrpCat.HasLimit.productLimitCone_cone_π`, `AddSubgroup.le_pi_iff`, `evalAddMonoidHom_apply`, `AddCommGrpCat.biproductIsoPi_inv_comp_π`, `AddCommGrpCat.coyonedaType_map_app`
`evalMonoidHom` 📖	CompOp	8 math math: `Submonoid.le_pi_iff`, `CommMonCat.coyonedaType_obj_map`, `evalMonoidHom_apply`, `CommGrpCat.coyonedaType_map_app`, `Subgroup.le_pi_iff`, `coe_evalMonoidHom`, `CommGrpCat.coyonedaType_obj_map`, `CommMonCat.coyonedaType_map_app`
`evalMulHom` 📖	CompOp	2 math math: `evalNonUnitalStarAlgHom_apply`, `evalMulHom_apply`
`monoidHom` 📖	CompOp	6 math math: `CommMonCat.coyonedaType_obj_map`, `CommGrpCat.coyonedaType_map_app`, `monoidHom_apply`, `CommGrpCat.coyonedaType_obj_map`, `monoidHom_injective`, `CommMonCat.coyonedaType_map_app`
`mulHom` 📖	CompOp	2 math math: `mulHom_injective`, `mulHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommute_iff` 📖	mathematical	—	`AddCommute` `instAdd`	—	`addSemiconjBy_iff`
`addHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `instAdd` `AddHom.funLike` `addHom`	—	—
`addHom_injective` 📖	mathematical	`DFunLike.coe` `AddHom` `AddHom.funLike`	`instAdd` `addHom`	—	—
`addMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom.instFunLike` `addMonoidHom`	—	—
`addMonoidHom_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`addZeroClass` `addMonoidHom`	—	`addHom_injective`
`addSemiconjBy_iff` 📖	mathematical	—	`AddSemiconjBy` `instAdd`	—	—
`coe_evalMonoidHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom.instFunLike` `evalMonoidHom` `Function.eval`	—	—
`commute_iff` 📖	mathematical	—	`Commute` `instMul`	—	`semiconjBy_iff`
`constAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `instAdd` `AddHom.funLike` `constAddHom`	—	—
`constAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom.instFunLike` `constAddMonoidHom`	—	—
`constMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom.instFunLike` `constMonoidHom`	—	—
`constMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `instMul` `MulHom.funLike` `constMulHom`	—	—
`evalAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `instAdd` `AddHom.funLike` `evalAddHom`	—	—
`evalAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `addZeroClass` `AddMonoidHom.instFunLike` `evalAddMonoidHom`	—	—
`evalMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom.instFunLike` `evalMonoidHom`	—	—
`evalMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `instMul` `MulHom.funLike` `evalMulHom`	—	—
`instIsAddTorsionFree` 📖	mathematical	`IsAddTorsionFree`	`addMonoid`	—	`nsmul_right_injective`
`instIsMulTorsionFree` 📖	mathematical	`IsMulTorsionFree`	`monoid`	—	`pow_left_injective`
`monoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `mulOneClass` `MonoidHom.instFunLike` `monoidHom`	—	—
`monoidHom_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`mulOneClass` `monoidHom`	—	`mulHom_injective`
`mulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `instMul` `MulHom.funLike` `mulHom`	—	—
`mulHom_injective` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike`	`instMul` `mulHom`	—	—
`mulSingle_apply_commute` 📖	mathematical	—	`Commute` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `mulSingle` `MulOne.toOne`	—	`Decidable.eq_or_ne` `mulSingle_commute`
`mulSingle_commute` 📖	mathematical	—	`Pairwise`	—	`mulSingle_eq_of_ne` `mul_one` `one_mul` `mulSingle_eq_of_ne'`
`mulSingle_comp_equiv` 📖	mathematical	—	`mulSingle` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`mulSingle_apply` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply`
`mulSingle_div` 📖	mathematical	—	`mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `instDiv`	—	`MonoidHom.map_div`
`mulSingle_inf` 📖	mathematical	—	`mulSingle` `SemilatticeInf.toMin` `instMinForall_mathlib`	—	`Function.update_inf`
`mulSingle_inv` 📖	mathematical	—	`mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toInv` `instInv`	—	`MonoidHom.map_inv`
`mulSingle_mono` 📖	mathematical	—	`Monotone` `preorder` `mulSingle`	—	`Function.update_mono`
`mulSingle_mul` 📖	mathematical	—	`mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `MulOne.toMul` `instMul`	—	`MonoidHom.map_mul`
`mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle` 📖	mathematical	—	`instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `mulSingle` `MulOne.toOne`	—	`mulSingle_apply` `mul_ite` `ite_mul` `one_mul` `mul_one`
`mulSingle_pow` 📖	mathematical	—	`mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow` `instPow`	—	`MonoidHom.map_pow`
`mulSingle_strictMono` 📖	mathematical	—	`StrictMono` `preorder` `mulSingle`	—	`Function.update_strictMono`
`mulSingle_sup` 📖	mathematical	—	`mulSingle` `SemilatticeSup.toMax` `instMaxForall_mathlib`	—	`Function.update_sup`
`mulSingle_zpow` 📖	mathematical	—	`mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `instPow`	—	`MonoidHom.map_zpow`
`one_anti` 📖	mathematical	—	`Antitone` `instOne`	—	`antitone_const`
`one_mono` 📖	mathematical	—	`Monotone` `instOne`	—	`monotone_const`
`semiconjBy_iff` 📖	mathematical	—	`SemiconjBy` `instMul`	—	—
`single_add` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `instAdd`	—	`AddMonoidHom.map_add`
`single_addCommute` 📖	mathematical	—	`Pairwise`	—	`single_eq_of_ne` `add_zero` `zero_add` `single_eq_of_ne'`
`single_add_single_eq_single_add_single` 📖	mathematical	—	`instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `single` `AddZero.toZero`	—	`single_apply` `add_ite` `ite_add` `zero_add` `add_zero`
`single_apply_addCommute` 📖	mathematical	—	`AddCommute` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `single` `AddZero.toZero`	—	`Decidable.eq_or_ne` `single_addCommute`
`single_comp_equiv` 📖	mathematical	—	`single` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`single_apply` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply`
`single_inf` 📖	mathematical	—	`single` `SemilatticeInf.toMin` `instMinForall_mathlib`	—	`Function.update_inf`
`single_mono` 📖	mathematical	—	`Monotone` `preorder` `single`	—	`Function.update_mono`
`single_neg` 📖	mathematical	—	`single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toNeg` `instNeg`	—	`AddMonoidHom.map_neg`
`single_nsmul` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul` `instSMul`	—	`AddMonoidHom.map_nsmul`
`single_strictMono` 📖	mathematical	—	`StrictMono` `preorder` `single`	—	`Function.update_strictMono`
`single_sub` 📖	mathematical	—	`single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instSub`	—	`AddMonoidHom.map_sub`
`single_sup` 📖	mathematical	—	`single` `SemilatticeSup.toMax` `instMaxForall_mathlib`	—	`Function.update_sup`
`single_zsmul` 📖	mathematical	—	`single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `instSMul`	—	`AddMonoidHom.map_zsmul`
`update_eq_div_mul_mulSingle` 📖	mathematical	—	`Function.update` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instDiv` `DivInvMonoid.toDiv` `mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`eq_or_ne` `Function.update_self` `mulSingle_eq_same` `div_self'` `one_mul` `Function.update_of_ne` `mulSingle_eq_of_ne'` `div_one` `mul_one`
`update_eq_sub_add_single` 📖	mathematical	—	`Function.update` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instSub` `SubNegMonoid.toSub` `single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`eq_or_ne` `Function.update_self` `single_eq_same` `sub_self` `zero_add` `Function.update_of_ne` `single_eq_of_ne'` `sub_zero` `add_zero`
`zero_anti` 📖	mathematical	—	`Antitone` `instZero`	—	`antitone_const`
`zero_mono` 📖	mathematical	—	`Monotone` `instZero`	—	`monotone_const`

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi` 📖	mathematical	`SemiconjBy`	`Pi.instMul`	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piecewise_add` 📖	mathematical	—	`piecewise` `Pi.instAdd`	—	`piecewise_op₂`
`piecewise_div` 📖	mathematical	—	`piecewise` `Pi.instDiv`	—	`piecewise_op₂`
`piecewise_inv` 📖	mathematical	—	`piecewise` `Pi.instInv`	—	`piecewise_op`
`piecewise_mul` 📖	mathematical	—	`piecewise` `Pi.instMul`	—	`piecewise_op₂`
`piecewise_neg` 📖	mathematical	—	`piecewise` `Pi.instNeg`	—	`piecewise_op`
`piecewise_sub` 📖	mathematical	—	`piecewise` `Pi.instSub`	—	`piecewise_op₂`
`preimage_one` 📖	mathematical	—	`preimage` `Pi.instOne` `Set` `instMembership` `univ` `instEmptyCollection`	—	`preimage_const`
`preimage_zero` 📖	mathematical	—	`preimage` `Pi.instZero` `Set` `instMembership` `univ` `instEmptyCollection`	—	`preimage_const`
`range_one` 📖	mathematical	—	`range` `Pi.instOne` `Set` `instSingletonSet`	—	`range_const`
`range_zero` 📖	mathematical	—	`range` `Pi.instZero` `Set` `instSingletonSet`	—	`range_const`

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curry_add` 📖	mathematical	—	`curry` `Pi.instAdd`	—	—
`curry_inv` 📖	mathematical	—	`curry` `Pi.instInv`	—	—
`curry_mul` 📖	mathematical	—	`curry` `Pi.instMul`	—	—
`curry_mulSingle` 📖	mathematical	—	`curry` `Pi.mulSingle` `instDecidableEqSigma` `Pi.instOne`	—	`curry_update`
`curry_neg` 📖	mathematical	—	`curry` `Pi.instNeg`	—	—
`curry_one` 📖	mathematical	—	`curry` `Pi.instOne`	—	—
`curry_single` 📖	mathematical	—	`curry` `Pi.single` `instDecidableEqSigma` `Pi.instZero`	—	`curry_update`
`curry_zero` 📖	mathematical	—	`curry` `Pi.instZero`	—	—
`uncurry_add` 📖	mathematical	—	`uncurry` `Pi.instAdd`	—	—
`uncurry_inv` 📖	mathematical	—	`uncurry` `Pi.instInv`	—	—
`uncurry_mul` 📖	mathematical	—	`uncurry` `Pi.instMul`	—	—
`uncurry_mulSingle_mulSingle` 📖	mathematical	—	`uncurry` `Pi.mulSingle` `Pi.instOne` `instDecidableEqSigma`	—	`curry_mulSingle` `uncurry_curry`
`uncurry_neg` 📖	mathematical	—	`uncurry` `Pi.instNeg`	—	—
`uncurry_one` 📖	mathematical	—	`uncurry` `Pi.instOne`	—	—
`uncurry_single_single` 📖	mathematical	—	`uncurry` `Pi.single` `Pi.instZero` `instDecidableEqSigma`	—	`curry_single` `uncurry_curry`
`uncurry_zero` 📖	mathematical	—	`uncurry` `Pi.instZero`	—	—

ZeroHom

Definitions

Name	Category	Theorems
`single` 📖	CompOp	2 math math: `single_apply`, `coe_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_single` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `Pi.instZero` `funLike` `single` `Pi.single`	—	—
`single_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `Pi.instZero` `funLike` `single` `Pi.single`	—	—

---

← Back to Index