Documentation Verification Report

Basic

📁 Source: Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean

Statistics

Metric	Count
Definitions `coinvariantsTensorObj`, `torIso`, `groupHomology`, `cycles`, `cyclesMk`, `iCycles`, `inhomogeneousChains`, `d`, `inhomogeneousChainsIso`, `toCycles`, `π`, `groupHomologyIso`, `groupHomologyIsoTor`	13
Theorems `Tor_map`, `Tor_obj`, `isZero_Tor_succ_of_projective`, `iCycles_mk`, `d_comp_d`, `d_def`, `d_eq`, `d_single`, `ext`, `ext_iff`, `groupHomology_induction_on`, `isZero_groupHomology_succ_of_subsingleton`	12
Total	25

HomologicalComplex

Definitions

Name	Category	Theorems
`coinvariantsTensorObj` 📖	CompOp	3 math math: `groupHomology.inhomogeneousChains.d_eq`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`

Rep

Definitions

Name	Category	Theorems
`torIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Tor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Tor` `CategoryTheory.NatTrans.leftDerived` `Action.instAbelian` `ModuleCat.abelian` `CategoryTheory.Functor.obj` `coinvariantsTensor`	—	—
`Tor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Tor` `CategoryTheory.Functor.leftDerived` `Action.instAbelian` `ModuleCat.abelian` `coinvariantsTensor`	—	—
`isZero_Tor_succ_of_projective` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Rep` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Tor`	—	`CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ`

(root)

Definitions

Name	Category	Theorems
`groupHomology` 📖	CompOp	43 math math: `groupHomology.π_comp_H2Iso_hom_assoc`, `groupHomology.map₁_quotientGroupMk'_epi`, `groupHomology.map₁_one`, `groupHomology.H0π_comp_map`, `groupHomology.map_id`, `groupHomology.δ₀_apply`, `groupHomology.π_comp_H0Iso_hom_assoc`, `Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff`, `groupHomology.map_comp`, `groupHomology.map_id_comp`, `groupHomology.functor_obj`, `groupHomology.map_comp_assoc`, `groupHomology.π_comp_H2Iso_hom`, `Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff`, `groupHomology.H1π_comp_map_apply`, `groupHomology.H0π_comp_map_assoc`, `groupHomology.π_comp_H0Iso_hom_apply`, `groupHomology.H2π_comp_map_assoc`, `groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply`, `groupHomology.π_comp_H0IsoOfIsTrivial_hom`, `groupHomology.map_id_comp_H0Iso_hom_assoc`, `groupHomology.π_comp_H1Iso_hom_apply`, `Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff`, `groupHomology.π_map_assoc`, `groupHomology.δ_apply`, `groupHomology.π_comp_H1Iso_hom_assoc`, `groupHomology.H2π_comp_map`, `groupHomology.H1π_comp_map_assoc`, `groupHomology.H1π_comp_map`, `groupHomology.map_id_comp_H0Iso_hom_apply`, `groupHomology.H2π_comp_map_apply`, `Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff`, `groupHomology.π_comp_H0Iso_hom`, `groupHomology.map_id_comp_H0Iso_hom`, `groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc`, `groupHomology.π_map_apply`, `groupHomology.π_comp_H2Iso_hom_apply`, `groupHomology.π_comp_H1Iso_hom`, `groupHomology.epi_map_0_of_epi`, `isZero_groupHomology_succ_of_subsingleton`, `groupHomology.π_map`, `groupHomology.H0π_comp_map_apply`, `groupHomology.δ₁_apply`
`groupHomologyIso` 📖	CompOp	—
`groupHomologyIsoTor` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`groupHomology_induction_on` 📖	—	`DFunLike.coe` `groupHomology.cycles` `groupHomology` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `groupHomology.π`	—	—	`ModuleCat.epi_iff_surjective` `HomologicalComplex.instEpiHomologyπ`
`isZero_groupHomology_succ_of_subsingleton` 📖	mathematical	—	`CategoryTheory.Limits.IsZero` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `groupHomology`	—	`CategoryTheory.Limits.IsZero.of_iso` `Rep.isZero_Tor_succ_of_projective` `Rep.trivial_projective_of_subsingleton`

groupHomology

Definitions

Name	Category	Theorems
`cycles` 📖	CompOp	60 math math: `π_comp_H2Iso_hom_assoc`, `cyclesIso₀_inv_comp_iCycles_apply`, `cyclesMap_id_comp`, `cyclesMap_comp_isoCycles₂_hom`, `toCycles_comp_isoCycles₂_hom_assoc`, `isoCycles₁_inv_comp_iCycles_apply`, `π_comp_H0Iso_hom_assoc`, `cyclesMap_comp_assoc`, `cyclesMap_comp_cyclesIso₀_hom_apply`, `toCycles_comp_isoCycles₁_hom_apply`, `cyclesIso₀_comp_H0π_apply`, `π_comp_H2Iso_hom`, `cyclesIso₀_inv_comp_cyclesMap_apply`, `toCycles_comp_isoCycles₁_hom_assoc`, `π_comp_H0Iso_hom_apply`, `π_comp_H0IsoOfIsTrivial_hom_apply`, `isoCycles₂_hom_comp_i_apply`, `π_comp_H0IsoOfIsTrivial_hom`, `cyclesMap_comp_isoCycles₂_hom_assoc`, `cyclesIso₀_inv_comp_iCycles`, `π_comp_H1Iso_hom_apply`, `toCycles_comp_isoCycles₂_hom`, `cyclesMap_comp_isoCycles₂_hom_apply`, `isoCycles₁_hom_comp_i_apply`, `cyclesMap_comp_cyclesIso₀_hom`, `cyclesMap_comp_isoCycles₁_hom_apply`, `toCycles_comp_isoCycles₂_hom_apply`, `π_map_assoc`, `δ_apply`, `isoCycles₂_inv_comp_iCycles_apply`, `isoCycles₂_inv_comp_iCycles_assoc`, `cyclesMk₂_eq`, `isoCycles₁_inv_comp_iCycles_assoc`, `π_comp_H1Iso_hom_assoc`, `cyclesIso₀_inv_comp_cyclesMap_assoc`, `cyclesMk₁_eq`, `cyclesIso₀_comp_H0π_assoc`, `π_comp_H0Iso_hom`, `cyclesIso₀_inv_comp_cyclesMap`, `isoCycles₁_hom_comp_i_assoc`, `π_comp_H0IsoOfIsTrivial_hom_assoc`, `π_map_apply`, `π_comp_H2Iso_hom_apply`, `isoCycles₁_inv_comp_iCycles`, `cyclesMap_comp_isoCycles₁_hom_assoc`, `toCycles_comp_isoCycles₁_hom`, `isoCycles₂_hom_comp_i`, `π_comp_H1Iso_hom`, `isoCycles₂_inv_comp_iCycles`, `cyclesIso₀_comp_H0π`, `iCycles_mk`, `cyclesMk₀_eq`, `isoCycles₁_hom_comp_i`, `cyclesMap_comp`, `cyclesMap_comp_cyclesIso₀_hom_assoc`, `cyclesIso₀_inv_comp_iCycles_assoc`, `cyclesMap_id`, `π_map`, `isoCycles₂_hom_comp_i_assoc`, `cyclesMap_comp_isoCycles₁_hom`
`cyclesMk` 📖	CompOp	5 math math: `δ_apply`, `cyclesMk₂_eq`, `cyclesMk₁_eq`, `iCycles_mk`, `cyclesMk₀_eq`
`iCycles` 📖	CompOp	16 math math: `cyclesIso₀_inv_comp_iCycles_apply`, `isoCycles₁_inv_comp_iCycles_apply`, `isoCycles₂_hom_comp_i_apply`, `cyclesIso₀_inv_comp_iCycles`, `isoCycles₁_hom_comp_i_apply`, `isoCycles₂_inv_comp_iCycles_apply`, `isoCycles₂_inv_comp_iCycles_assoc`, `isoCycles₁_inv_comp_iCycles_assoc`, `isoCycles₁_hom_comp_i_assoc`, `isoCycles₁_inv_comp_iCycles`, `isoCycles₂_hom_comp_i`, `isoCycles₂_inv_comp_iCycles`, `iCycles_mk`, `isoCycles₁_hom_comp_i`, `cyclesIso₀_inv_comp_iCycles_assoc`, `isoCycles₂_hom_comp_i_assoc`
`inhomogeneousChains` 📖	CompOp	71 math math: `chainsMap_f_3_comp_chainsIso₃_apply`, `eq_d₃₂_comp_inv`, `chainsMap_id`, `comp_d₂₁_eq`, `toCycles_comp_isoCycles₂_hom_assoc`, `chainsMap_id_f_map_mono`, `d₁₀ArrowIso_hom_left`, `chainsMap_f_3_comp_chainsIso₃`, `eq_d₂₁_comp_inv`, `inhomogeneousChains.d_def`, `coinvariantsMk_comp_opcyclesIso₀_inv_assoc`, `chainsMap_f_single`, `eq_d₃₂_comp_inv_apply`, `pOpcycles_comp_opcyclesIso_hom_apply`, `chainsMap_f_map_epi`, `isoShortComplexH1_hom`, `comp_d₁₀_eq`, `toCycles_comp_isoCycles₁_hom_assoc`, `chainsFunctor_obj`, `d₁₀ArrowIso_inv_right`, `chainsMap_id_f_map_epi`, `chainsMap_id_comp`, `eq_d₂₁_comp_inv_assoc`, `cyclesIso₀_inv_comp_iCycles`, `chainsMap_id_f_hom_eq_mapRange`, `toCycles_comp_isoCycles₂_hom`, `chainsMap_f_map_mono`, `eq_d₁₀_comp_inv`, `isoShortComplexH1_inv`, `eq_d₁₀_comp_inv_assoc`, `chainsMap_f_1_comp_chainsIso₁_assoc`, `lsingle_comp_chainsMap_f`, `coinvariantsMk_comp_opcyclesIso₀_inv_apply`, `chainsMap_comp`, `chainsMap_f_3_comp_chainsIso₃_assoc`, `chainsMap_f_0_comp_chainsIso₀_assoc`, `eq_d₃₂_comp_inv_assoc`, `isoCycles₂_inv_comp_iCycles_assoc`, `isoShortComplexH2_hom`, `cyclesMk₂_eq`, `chainsMap_f_1_comp_chainsIso₁`, `isoCycles₁_inv_comp_iCycles_assoc`, `chainsMap_f_2_comp_chainsIso₂`, `pOpcycles_comp_opcyclesIso_hom`, `coinvariantsMk_comp_opcyclesIso₀_inv`, `chainsMap_f_hom`, `pOpcycles_comp_opcyclesIso_hom_assoc`, `cyclesMk₁_eq`, `isoCycles₁_hom_comp_i_assoc`, `isoCycles₁_inv_comp_iCycles`, `chainsMap_zero`, `isoShortComplexH2_inv`, `toCycles_comp_isoCycles₁_hom`, `chainsMap_f_2_comp_chainsIso₂_assoc`, `isoCycles₂_hom_comp_i`, `isoCycles₂_inv_comp_iCycles`, `d₁₀ArrowIso_hom_right`, `eq_d₂₁_comp_inv_apply`, `cyclesMk₀_eq`, `isoCycles₁_hom_comp_i`, `chainsMap_f_0_comp_chainsIso₀_apply`, `lsingle_comp_chainsMap_f_assoc`, `cyclesIso₀_inv_comp_iCycles_assoc`, `d₁₀ArrowIso_inv_left`, `eq_d₁₀_comp_inv_apply`, `chainsMap_f_1_comp_chainsIso₁_apply`, `isoCycles₂_hom_comp_i_assoc`, `comp_d₃₂_eq`, `chainsMap_f_0_comp_chainsIso₀`, `chainsMap_f`, `chainsMap_f_2_comp_chainsIso₂_apply`
`inhomogeneousChainsIso` 📖	CompOp	—
`toCycles` 📖	CompOp	6 math math: `toCycles_comp_isoCycles₂_hom_assoc`, `toCycles_comp_isoCycles₁_hom_apply`, `toCycles_comp_isoCycles₁_hom_assoc`, `toCycles_comp_isoCycles₂_hom`, `toCycles_comp_isoCycles₂_hom_apply`, `toCycles_comp_isoCycles₁_hom`
`π` 📖	CompOp	19 math math: `π_comp_H2Iso_hom_assoc`, `π_comp_H0Iso_hom_assoc`, `cyclesIso₀_comp_H0π_apply`, `π_comp_H2Iso_hom`, `π_comp_H0Iso_hom_apply`, `π_comp_H0IsoOfIsTrivial_hom_apply`, `π_comp_H0IsoOfIsTrivial_hom`, `π_comp_H1Iso_hom_apply`, `π_map_assoc`, `δ_apply`, `π_comp_H1Iso_hom_assoc`, `cyclesIso₀_comp_H0π_assoc`, `π_comp_H0Iso_hom`, `π_comp_H0IsoOfIsTrivial_hom_assoc`, `π_map_apply`, `π_comp_H2Iso_hom_apply`, `π_comp_H1Iso_hom`, `cyclesIso₀_comp_H0π`, `π_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iCycles_mk` 📖	mathematical	`ComplexShape.next` `ComplexShape.down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `DFunLike.coe` `HomologicalComplex.X` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `inhomogeneousChains` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `HomologicalComplex.d` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`cycles` `iCycles` `cyclesMk`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.i_cyclesMk` `ModuleCat.forget₂_addCommGrp_additive` `CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier`

groupHomology.inhomogeneousChains

Definitions

Name	Category	Theorems
`d` 📖	CompOp	4 math math: `d_def`, `d_single`, `d_comp_d`, `d_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`d_comp_d` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.of` `Finsupp` `ModuleCat.carrier` `Action.V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Finsupp.instAddCommGroup` `Finsupp.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `ModuleCat.instZeroHom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.id_comp` `HomologicalComplex.d_comp_d`
`d_def` 📖	mathematical	—	`HomologicalComplex.d` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `groupHomology.inhomogeneousChains` `d`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `ChainComplex.of_d`
`d_eq` 📖	mathematical	—	`d` `CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.of` `Finsupp` `ModuleCat.carrier` `Action.V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Finsupp.instAddCommGroup` `Finsupp.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `Representation.Coinvariants` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `Rep` `Action.instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `Action.instMonoidalCategory` `ModuleCat.monoidalCategory` `Rep.free` `ModuleCat.isAddCommGroup` `Rep.ρ` `Representation.Coinvariants.instAddCommGroup` `Representation.Coinvariants.instModule` `CategoryTheory.Iso.inv` `LinearEquiv.toModuleIso` `Rep.coinvariantsTensorFreeLEquiv` `Fintype.decidablePiFintype` `Fin.fintype` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.coinvariantsTensorObj` `Rep.barComplex` `HomologicalComplex.d` `CategoryTheory.Iso.hom`	—	`ModuleCat.hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finsupp.lhom_ext'` `LinearMap.ext` `RingHomCompTriple.ids` `d_single` `Finset.sum_congr` `Finsupp.smul_single` `LinearMap.comp.congr_simp` `Rep.barComplex.d_def` `Rep.finsuppToCoinvariantsTensorFree_single` `Rep.barComplex.d_single` `TensorProduct.tmul_add` `TensorProduct.tmul_sum` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single` `one_smul` `inv_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass`
`d_single` 📖	mathematical	—	`DFunLike.coe` `ModuleCat.of` `CommRing.toRing` `Finsupp` `ModuleCat.carrier` `Action.V` `ModuleCat` `ModuleCat.moduleCategory` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Finsupp.instAddCommGroup` `Finsupp.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.isAddCommGroup` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `d` `Finsupp.single` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `Rep.ρ` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Finset.sum` `Finsupp.instAddCommMonoid` `Finset.univ` `Fin.fintype` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Monoid.toNatPow` `NegZeroClass.toNeg` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Fin.contractNth` `MulOne.toMul`	—	`Finsupp.sum_single_index` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.single_zero` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_congr` `smul_zero` `Finset.sum_const_zero` `add_zero` `Finsupp.smul_single`
`ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.of` `ModuleCat.carrier` `Action.V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `ModuleCat.isModule` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommGroup` `Finsupp.module` `Ring.toSemiring` `ModuleCat.ofHom` `Finsupp.lsingle`	—	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `ModuleCat.hom_ext` `Finsupp.lhom_ext'` `RingHomCompTriple.ids` `ModuleCat.hom_ext_iff`
`ext_iff` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.of` `ModuleCat.carrier` `Action.V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `ModuleCat.isModule` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommGroup` `Finsupp.module` `Ring.toSemiring` `ModuleCat.ofHom` `Finsupp.lsingle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `ext`

---

← Back to Index