LowDegree

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

Statistics

Metric	Count
Definitions H0, H0Iso, H0IsoOfIsTrivial, H0π, H1AddEquivOfIsTrivial, H1Iso, H1ToTensorOfIsTrivial, H1π, H2, H2Iso, H2π, IsBoundary₀, IsBoundary₁, IsBoundary₂, IsCycle₁, IsCycle₂, boundariesOfIsBoundary₁, boundariesOfIsBoundary₂, boundariesToCycles₁, boundariesToCycles₂, boundaries₁, boundaries₂, chainsIso₀, chainsIso₁, chainsIso₂, chainsIso₃, chains₁ToCoinvariantsKer, coinvariantsKerOfIsBoundary₀, cyclesIso₀, cyclesOfIsCycle₁, cyclesOfIsCycle₂, cycles₁, cycles₁IsoOfIsTrivial, cycles₂, d₁₀, d₁₀ArrowIso, d₂₁, d₃₂, isoCycles₁, isoCycles₂, isoShortComplexH1, isoShortComplexH2, mkH1OfIsTrivial, opcyclesIso₀, shortComplexH0, shortComplexH1, shortComplexH2	47
Theorems H0IsoOfIsTrivial_inv_eq_π, H0_induction_on, H0π_comp_H0Iso_hom, H0π_comp_H0Iso_hom_apply, H0π_comp_H0Iso_hom_assoc, H1AddEquivOfIsTrivial_apply, H1AddEquivOfIsTrivial_single, H1AddEquivOfIsTrivial_symm_apply, H1AddEquivOfIsTrivial_symm_tmul, H1ToTensorOfIsTrivial_H1π_single, H1_induction_on, H1π_eq_iff, H1π_eq_zero_iff, H2_induction_on, H2π_eq_iff, H2π_eq_zero_iff, boundariesOfIsBoundary₁_coe, boundariesOfIsBoundary₂_coe, boundariesToCycles₁_apply, boundariesToCycles₂_apply, boundaries₁_le_cycles₁, boundaries₂_le_cycles₂, chains₁ToCoinvariantsKer_surjective, coinvariantsKerOfIsBoundary₀_coe, coinvariantsMk_comp_H0Iso_inv, coinvariantsMk_comp_H0Iso_inv_apply, coinvariantsMk_comp_H0Iso_inv_assoc, coinvariantsMk_comp_opcyclesIso₀_inv, coinvariantsMk_comp_opcyclesIso₀_inv_apply, coinvariantsMk_comp_opcyclesIso₀_inv_assoc, comp_d₁₀_eq, comp_d₂₁_eq, comp_d₃₂_eq, cyclesIso₀_comp_H0π, cyclesIso₀_comp_H0π_apply, cyclesIso₀_comp_H0π_assoc, cyclesIso₀_inv_comp_iCycles, cyclesIso₀_inv_comp_iCycles_apply, cyclesIso₀_inv_comp_iCycles_assoc, cyclesMk₀_eq, cyclesMk₁_eq, cyclesMk₂_eq, cyclesOfIsCycle₁_coe, cyclesOfIsCycle₂_coe, cycles₁IsoOfIsTrivial_hom_apply, cycles₁IsoOfIsTrivial_inv_apply, cycles₁_eq_top_of_isTrivial, d₁₀ArrowIso_hom_left, d₁₀ArrowIso_hom_right, d₁₀ArrowIso_inv_left, d₁₀ArrowIso_inv_right, d₁₀_comp_coinvariantsMk, d₁₀_comp_coinvariantsMk_apply, d₁₀_comp_coinvariantsMk_assoc, d₁₀_eq_zero_of_isTrivial, d₁₀_single, d₁₀_single_inv, d₁₀_single_one, d₂₁_apply_mem_cycles₁, d₂₁_comp_d₁₀, d₂₁_comp_d₁₀_apply, d₂₁_comp_d₁₀_assoc, d₂₁_single, d₂₁_single_inv_mul_ρ_add_single, d₂₁_single_inv_self_ρ_sub_self_inv, d₂₁_single_one_fst, d₂₁_single_one_snd, d₂₁_single_self_inv_ρ_sub_inv_self, d₂₁_single_ρ_add_single_inv_mul, d₃₂_apply_mem_cycles₂, d₃₂_comp_d₂₁, d₃₂_comp_d₂₁_apply, d₃₂_comp_d₂₁_assoc, d₃₂_single, d₃₂_single_one_fst, d₃₂_single_one_snd, d₃₂_single_one_thd, eq_d₁₀_comp_inv, eq_d₁₀_comp_inv_apply, eq_d₁₀_comp_inv_assoc, eq_d₂₁_comp_inv, eq_d₂₁_comp_inv_apply, eq_d₂₁_comp_inv_assoc, eq_d₃₂_comp_inv, eq_d₃₂_comp_inv_apply, eq_d₃₂_comp_inv_assoc, instEpiModuleCatGShortComplexH0, instEpiModuleCatH0π, instEpiModuleCatH1π, instEpiModuleCatH2π, isBoundary₀_iff, isBoundary₀_of_mem_coinvariantsKer, isBoundary₁_iff, isBoundary₁_of_mem_boundaries₁, isBoundary₂_iff, isBoundary₂_of_mem_boundaries₂, isCycle₁_of_mem_cycles₁, isCycle₂_of_mem_cycles₂, isoCycles₁_hom_comp_i, isoCycles₁_hom_comp_i_apply, isoCycles₁_hom_comp_i_assoc, isoCycles₁_inv_comp_iCycles, isoCycles₁_inv_comp_iCycles_apply, isoCycles₁_inv_comp_iCycles_assoc, isoCycles₂_hom_comp_i, isoCycles₂_hom_comp_i_apply, isoCycles₂_hom_comp_i_assoc, isoCycles₂_inv_comp_iCycles, isoCycles₂_inv_comp_iCycles_apply, isoCycles₂_inv_comp_iCycles_assoc, isoShortComplexH1_hom, isoShortComplexH1_inv, isoShortComplexH2_hom, isoShortComplexH2_inv, mem_cycles₁_iff, mem_cycles₁_of_mem_boundaries₁, mem_cycles₂_iff, mem_cycles₂_of_mem_boundaries₂, mkH1OfIsTrivial_apply, pOpcycles_comp_opcyclesIso_hom, pOpcycles_comp_opcyclesIso_hom_apply, pOpcycles_comp_opcyclesIso_hom_assoc, range_d₁₀_eq_coinvariantsKer, shortComplexH0_exact, shortComplexH0_f, shortComplexH0_g, shortComplexH1_f, shortComplexH1_g, shortComplexH2_f, shortComplexH2_g, single_inv_ρ_self_add_single_mem_boundaries₁, single_isCycle₁_iff, single_isCycle₁_of_mem_fixedPoints, single_isCycle₂_iff, single_isCycle₂_iff_inv, single_mem_cycles₁_iff, single_mem_cycles₁_of_mem_invariants, single_mem_cycles₂_iff, single_mem_cycles₂_iff_inv, single_one_fst_sub_single_one_fst_mem_boundaries₂, single_one_fst_sub_single_one_snd_mem_boundaries₂, single_one_mem_boundaries₁, single_one_snd_sub_single_one_fst_mem_boundaries₂, single_one_snd_sub_single_one_snd_mem_boundaries₂, single_ρ_self_add_single_inv_mem_boundaries₁, toCycles_comp_isoCycles₁_hom, toCycles_comp_isoCycles₁_hom_apply, toCycles_comp_isoCycles₁_hom_assoc, toCycles_comp_isoCycles₂_hom, toCycles_comp_isoCycles₂_hom_apply, toCycles_comp_isoCycles₂_hom_assoc, π_comp_H0IsoOfIsTrivial_hom, π_comp_H0IsoOfIsTrivial_hom_apply, π_comp_H0IsoOfIsTrivial_hom_assoc, π_comp_H0Iso_hom, π_comp_H0Iso_hom_apply, π_comp_H0Iso_hom_assoc, π_comp_H1Iso_hom, π_comp_H1Iso_hom_apply, π_comp_H1Iso_hom_assoc, π_comp_H1Iso_inv, π_comp_H1Iso_inv_apply, π_comp_H1Iso_inv_assoc, π_comp_H2Iso_hom, π_comp_H2Iso_hom_apply, π_comp_H2Iso_hom_assoc, π_comp_H2Iso_inv, π_comp_H2Iso_inv_apply, π_comp_H2Iso_inv_assoc	169
Total	216

groupHomology

Definitions

Name	Category	Theorems
H0 📖	CompOp	24 math math: coinvariantsMk_comp_H0Iso_inv_apply, H0IsoOfIsTrivial_inv_eq_π, H0π_comp_map, δ₀_apply, π_comp_H0Iso_hom_assoc, coinvariantsMk_comp_H0Iso_inv, cyclesIso₀_comp_H0π_apply, H0π_comp_map_assoc, π_comp_H0Iso_hom_apply, π_comp_H0IsoOfIsTrivial_hom_apply, π_comp_H0IsoOfIsTrivial_hom, map_id_comp_H0Iso_hom_assoc, map_id_comp_H0Iso_hom_apply, cyclesIso₀_comp_H0π_assoc, instEpiModuleCatH0π, π_comp_H0Iso_hom, H0π_comp_H0Iso_hom, map_id_comp_H0Iso_hom, π_comp_H0IsoOfIsTrivial_hom_assoc, cyclesIso₀_comp_H0π, H0π_comp_H0Iso_hom_assoc, H0π_comp_H0Iso_hom_apply, coinvariantsMk_comp_H0Iso_inv_assoc, H0π_comp_map_apply
H0Iso 📖	CompOp	12 math math: coinvariantsMk_comp_H0Iso_inv_apply, π_comp_H0Iso_hom_assoc, coinvariantsMk_comp_H0Iso_inv, π_comp_H0Iso_hom_apply, map_id_comp_H0Iso_hom_assoc, map_id_comp_H0Iso_hom_apply, π_comp_H0Iso_hom, H0π_comp_H0Iso_hom, map_id_comp_H0Iso_hom, H0π_comp_H0Iso_hom_assoc, H0π_comp_H0Iso_hom_apply, coinvariantsMk_comp_H0Iso_inv_assoc
H0IsoOfIsTrivial 📖	CompOp	4 math math: H0IsoOfIsTrivial_inv_eq_π, π_comp_H0IsoOfIsTrivial_hom_apply, π_comp_H0IsoOfIsTrivial_hom, π_comp_H0IsoOfIsTrivial_hom_assoc
H0π 📖	CompOp	15 math math: coinvariantsMk_comp_H0Iso_inv_apply, H0IsoOfIsTrivial_inv_eq_π, H0π_comp_map, δ₀_apply, coinvariantsMk_comp_H0Iso_inv, cyclesIso₀_comp_H0π_apply, H0π_comp_map_assoc, cyclesIso₀_comp_H0π_assoc, instEpiModuleCatH0π, H0π_comp_H0Iso_hom, cyclesIso₀_comp_H0π, H0π_comp_H0Iso_hom_assoc, H0π_comp_H0Iso_hom_apply, coinvariantsMk_comp_H0Iso_inv_assoc, H0π_comp_map_apply
H1AddEquivOfIsTrivial 📖	CompOp	4 math math: H1AddEquivOfIsTrivial_single, H1AddEquivOfIsTrivial_symm_apply, H1AddEquivOfIsTrivial_apply, H1AddEquivOfIsTrivial_symm_tmul
H1Iso 📖	CompOp	6 math math: π_comp_H1Iso_inv, π_comp_H1Iso_hom_apply, π_comp_H1Iso_hom_assoc, π_comp_H1Iso_hom, π_comp_H1Iso_inv_apply, π_comp_H1Iso_inv_assoc
H1ToTensorOfIsTrivial 📖	CompOp	2 math math: H1ToTensorOfIsTrivial_H1π_single, H1AddEquivOfIsTrivial_apply
H1π 📖	CompOp	15 math math: δ₀_apply, π_comp_H1Iso_inv, H1π_comp_map_apply, H1AddEquivOfIsTrivial_single, H1ToTensorOfIsTrivial_H1π_single, H1π_eq_zero_iff, H1π_comp_map_assoc, instEpiModuleCatH1π, H1π_comp_map, mkH1OfIsTrivial_apply, π_comp_H1Iso_inv_apply, H1AddEquivOfIsTrivial_symm_tmul, π_comp_H1Iso_inv_assoc, δ₁_apply, H1π_eq_iff
H2 📖	CompOp	13 math math: π_comp_H2Iso_hom_assoc, π_comp_H2Iso_inv_assoc, π_comp_H2Iso_hom, H2π_comp_map_assoc, H2π_eq_iff, H2π_comp_map, π_comp_H2Iso_inv, instEpiModuleCatH2π, H2π_comp_map_apply, π_comp_H2Iso_hom_apply, π_comp_H2Iso_inv_apply, H2π_eq_zero_iff, δ₁_apply
H2Iso 📖	CompOp	6 math math: π_comp_H2Iso_hom_assoc, π_comp_H2Iso_inv_assoc, π_comp_H2Iso_hom, π_comp_H2Iso_inv, π_comp_H2Iso_hom_apply, π_comp_H2Iso_inv_apply
H2π 📖	CompOp	10 math math: π_comp_H2Iso_inv_assoc, H2π_comp_map_assoc, H2π_eq_iff, H2π_comp_map, π_comp_H2Iso_inv, instEpiModuleCatH2π, H2π_comp_map_apply, π_comp_H2Iso_inv_apply, H2π_eq_zero_iff, δ₁_apply
IsBoundary₀ 📖	MathDef	2 math math: isBoundary₀_of_mem_coinvariantsKer, isBoundary₀_iff
IsBoundary₁ 📖	MathDef	2 math math: isBoundary₁_of_mem_boundaries₁, isBoundary₁_iff
IsBoundary₂ 📖	MathDef	2 math math: isBoundary₂_of_mem_boundaries₂, isBoundary₂_iff
IsCycle₁ 📖	MathDef	3 math math: isCycle₁_of_mem_cycles₁, single_isCycle₁_iff, single_isCycle₁_of_mem_fixedPoints
IsCycle₂ 📖	MathDef	3 math math: single_isCycle₂_iff_inv, isCycle₂_of_mem_cycles₂, single_isCycle₂_iff
boundariesOfIsBoundary₁ 📖	CompOp	1 math math: boundariesOfIsBoundary₁_coe
boundariesOfIsBoundary₂ 📖	CompOp	1 math math: boundariesOfIsBoundary₂_coe
boundariesToCycles₁ 📖	CompOp	1 math math: boundariesToCycles₁_apply
boundariesToCycles₂ 📖	CompOp	1 math math: boundariesToCycles₂_apply
boundaries₁ 📖	CompOp	8 math math: boundariesOfIsBoundary₁_coe, single_ρ_self_add_single_inv_mem_boundaries₁, H1π_eq_zero_iff, single_one_mem_boundaries₁, single_inv_ρ_self_add_single_mem_boundaries₁, boundaries₁_le_cycles₁, boundariesToCycles₁_apply, H1π_eq_iff
boundaries₂ 📖	CompOp	9 math math: boundaries₂_le_cycles₂, single_one_snd_sub_single_one_fst_mem_boundaries₂, single_one_fst_sub_single_one_snd_mem_boundaries₂, single_one_fst_sub_single_one_fst_mem_boundaries₂, H2π_eq_iff, single_one_snd_sub_single_one_snd_mem_boundaries₂, boundariesOfIsBoundary₂_coe, boundariesToCycles₂_apply, H2π_eq_zero_iff
chainsIso₀ 📖	CompOp	21 math math: cyclesIso₀_inv_comp_iCycles_apply, coinvariantsMk_comp_opcyclesIso₀_inv_assoc, pOpcycles_comp_opcyclesIso_hom_apply, isoShortComplexH1_hom, comp_d₁₀_eq, d₁₀ArrowIso_inv_right, cyclesIso₀_inv_comp_iCycles, eq_d₁₀_comp_inv, isoShortComplexH1_inv, eq_d₁₀_comp_inv_assoc, coinvariantsMk_comp_opcyclesIso₀_inv_apply, chainsMap_f_0_comp_chainsIso₀_assoc, pOpcycles_comp_opcyclesIso_hom, coinvariantsMk_comp_opcyclesIso₀_inv, pOpcycles_comp_opcyclesIso_hom_assoc, d₁₀ArrowIso_hom_right, cyclesMk₀_eq, chainsMap_f_0_comp_chainsIso₀_apply, cyclesIso₀_inv_comp_iCycles_assoc, eq_d₁₀_comp_inv_apply, chainsMap_f_0_comp_chainsIso₀
chainsIso₁ 📖	CompOp	24 math math: comp_d₂₁_eq, isoCycles₁_inv_comp_iCycles_apply, d₁₀ArrowIso_hom_left, eq_d₂₁_comp_inv, isoShortComplexH1_hom, comp_d₁₀_eq, eq_d₂₁_comp_inv_assoc, eq_d₁₀_comp_inv, isoShortComplexH1_inv, eq_d₁₀_comp_inv_assoc, chainsMap_f_1_comp_chainsIso₁_assoc, isoCycles₁_hom_comp_i_apply, isoShortComplexH2_hom, chainsMap_f_1_comp_chainsIso₁, isoCycles₁_inv_comp_iCycles_assoc, cyclesMk₁_eq, isoCycles₁_hom_comp_i_assoc, isoCycles₁_inv_comp_iCycles, isoShortComplexH2_inv, eq_d₂₁_comp_inv_apply, isoCycles₁_hom_comp_i, d₁₀ArrowIso_inv_left, eq_d₁₀_comp_inv_apply, chainsMap_f_1_comp_chainsIso₁_apply
chainsIso₂ 📖	CompOp	25 math math: eq_d₃₂_comp_inv, comp_d₂₁_eq, eq_d₂₁_comp_inv, toCycles_comp_isoCycles₁_hom_apply, eq_d₃₂_comp_inv_apply, isoShortComplexH1_hom, toCycles_comp_isoCycles₁_hom_assoc, isoCycles₂_hom_comp_i_apply, eq_d₂₁_comp_inv_assoc, isoShortComplexH1_inv, eq_d₃₂_comp_inv_assoc, isoCycles₂_inv_comp_iCycles_apply, isoCycles₂_inv_comp_iCycles_assoc, isoShortComplexH2_hom, cyclesMk₂_eq, chainsMap_f_2_comp_chainsIso₂, isoShortComplexH2_inv, toCycles_comp_isoCycles₁_hom, chainsMap_f_2_comp_chainsIso₂_assoc, isoCycles₂_hom_comp_i, isoCycles₂_inv_comp_iCycles, eq_d₂₁_comp_inv_apply, isoCycles₂_hom_comp_i_assoc, comp_d₃₂_eq, chainsMap_f_2_comp_chainsIso₂_apply
chainsIso₃ 📖	CompOp	12 math math: chainsMap_f_3_comp_chainsIso₃_apply, eq_d₃₂_comp_inv, toCycles_comp_isoCycles₂_hom_assoc, chainsMap_f_3_comp_chainsIso₃, eq_d₃₂_comp_inv_apply, toCycles_comp_isoCycles₂_hom, chainsMap_f_3_comp_chainsIso₃_assoc, toCycles_comp_isoCycles₂_hom_apply, eq_d₃₂_comp_inv_assoc, isoShortComplexH2_hom, isoShortComplexH2_inv, comp_d₃₂_eq
chains₁ToCoinvariantsKer 📖	CompOp	1 math math: chains₁ToCoinvariantsKer_surjective
coinvariantsKerOfIsBoundary₀ 📖	CompOp	1 math math: coinvariantsKerOfIsBoundary₀_coe
cyclesIso₀ 📖	CompOp	19 math math: cyclesIso₀_inv_comp_iCycles_apply, π_comp_H0Iso_hom_assoc, cyclesMap_comp_cyclesIso₀_hom_apply, cyclesIso₀_comp_H0π_apply, cyclesIso₀_inv_comp_cyclesMap_apply, π_comp_H0Iso_hom_apply, π_comp_H0IsoOfIsTrivial_hom_apply, π_comp_H0IsoOfIsTrivial_hom, cyclesIso₀_inv_comp_iCycles, cyclesMap_comp_cyclesIso₀_hom, cyclesIso₀_inv_comp_cyclesMap_assoc, cyclesIso₀_comp_H0π_assoc, π_comp_H0Iso_hom, cyclesIso₀_inv_comp_cyclesMap, π_comp_H0IsoOfIsTrivial_hom_assoc, cyclesIso₀_comp_H0π, cyclesMk₀_eq, cyclesMap_comp_cyclesIso₀_hom_assoc, cyclesIso₀_inv_comp_iCycles_assoc
cyclesOfIsCycle₁ 📖	CompOp	1 math math: cyclesOfIsCycle₁_coe
cyclesOfIsCycle₂ 📖	CompOp	1 math math: cyclesOfIsCycle₂_coe
cycles₁ 📖	CompOp	51 math math: mapCycles₁_comp_apply, mapCycles₁_comp_assoc, mem_cycles₁_of_comp_eq_d₂₁, isoCycles₁_inv_comp_iCycles_apply, cycles₁_eq_top_of_isTrivial, cycles₁IsoOfIsTrivial_hom_apply, mapCycles₁_id_comp_assoc, mapCycles₁_comp, mapCycles₁_comp_i, toCycles_comp_isoCycles₁_hom_apply, mapCycles₁_id_comp_apply, mapCycles₁_comp_i_apply, H1π_comp_map_apply, toCycles_comp_isoCycles₁_hom_assoc, H1AddEquivOfIsTrivial_single, π_comp_H1Iso_hom_apply, mapCycles₁_id_comp, isoCycles₁_hom_comp_i_apply, H1ToTensorOfIsTrivial_H1π_single, cyclesOfIsCycle₁_coe, d₂₁_apply_mem_cycles₁, cyclesMap_comp_isoCycles₁_hom_apply, mem_cycles₁_of_mem_boundaries₁, H1π_eq_zero_iff, isoCycles₁_inv_comp_iCycles_assoc, π_comp_H1Iso_hom_assoc, H1π_comp_map_assoc, instEpiModuleCatH1π, H1π_comp_map, cyclesMk₁_eq, isoCycles₁_hom_comp_i_assoc, mapCycles₁_hom, isoCycles₁_inv_comp_iCycles, cyclesMap_comp_isoCycles₁_hom_assoc, single_mem_cycles₁_of_mem_invariants, coe_mapCycles₁, toCycles_comp_isoCycles₁_hom, π_comp_H1Iso_hom, mkH1OfIsTrivial_apply, cycles₁IsoOfIsTrivial_inv_apply, isoCycles₁_hom_comp_i, boundaries₁_le_cycles₁, H1AddEquivOfIsTrivial_symm_tmul, single_mem_cycles₁_iff, mapCycles₁_quotientGroupMk'_epi, mapCycles₁_comp_i_assoc, mem_cycles₁_iff, boundariesToCycles₁_apply, δ₁_apply, H1π_eq_iff, cyclesMap_comp_isoCycles₁_hom
cycles₁IsoOfIsTrivial 📖	CompOp	6 math math: cycles₁IsoOfIsTrivial_hom_apply, H1AddEquivOfIsTrivial_single, H1ToTensorOfIsTrivial_H1π_single, mkH1OfIsTrivial_apply, cycles₁IsoOfIsTrivial_inv_apply, H1AddEquivOfIsTrivial_symm_tmul
cycles₂ 📖	CompOp	41 math math: π_comp_H2Iso_hom_assoc, mapCycles₂_comp_assoc, boundaries₂_le_cycles₂, mem_cycles₂_iff, cyclesMap_comp_isoCycles₂_hom, toCycles_comp_isoCycles₂_hom_assoc, mapCycles₂_id_comp, mapCycles₂_comp_i, π_comp_H2Iso_hom, mapCycles₂_comp, coe_mapCycles₂, H2π_comp_map_assoc, mapCycles₂_comp_apply, H2π_eq_iff, isoCycles₂_hom_comp_i_apply, cyclesMap_comp_isoCycles₂_hom_assoc, mapCycles₂_id_comp_assoc, toCycles_comp_isoCycles₂_hom, cyclesMap_comp_isoCycles₂_hom_apply, toCycles_comp_isoCycles₂_hom_apply, mapCycles₂_hom, isoCycles₂_inv_comp_iCycles_apply, isoCycles₂_inv_comp_iCycles_assoc, cyclesMk₂_eq, H2π_comp_map, mem_cycles₂_of_mem_boundaries₂, instEpiModuleCatH2π, d₃₂_apply_mem_cycles₂, mapCycles₂_comp_i_assoc, mapCycles₂_id_comp_apply, H2π_comp_map_apply, π_comp_H2Iso_hom_apply, mapCycles₂_comp_i_apply, boundariesToCycles₂_apply, cyclesOfIsCycle₂_coe, isoCycles₂_hom_comp_i, isoCycles₂_inv_comp_iCycles, single_mem_cycles₂_iff, single_mem_cycles₂_iff_inv, isoCycles₂_hom_comp_i_assoc, H2π_eq_zero_iff
d₁₀ 📖	CompOp	21 math math: d₁₀_single_one, d₁₀ArrowIso_hom_left, d₁₀_comp_coinvariantsMk_apply, comp_d₁₀_eq, d₁₀ArrowIso_inv_right, d₁₀_comp_coinvariantsMk, d₂₁_comp_d₁₀_apply, range_d₁₀_eq_coinvariantsKer, shortComplexH0_f, eq_d₁₀_comp_inv, eq_d₁₀_comp_inv_assoc, d₂₁_comp_d₁₀, d₁₀_eq_zero_of_isTrivial, d₁₀_single_inv, d₁₀ArrowIso_hom_right, d₁₀_comp_coinvariantsMk_assoc, shortComplexH1_g, d₁₀ArrowIso_inv_left, eq_d₁₀_comp_inv_apply, d₂₁_comp_d₁₀_assoc, d₁₀_single
d₁₀ArrowIso 📖	CompOp	4 math math: d₁₀ArrowIso_hom_left, d₁₀ArrowIso_inv_right, d₁₀ArrowIso_hom_right, d₁₀ArrowIso_inv_left
d₂₁ 📖	CompOp	20 math math: shortComplexH1_f, comp_d₂₁_eq, d₃₂_comp_d₂₁_assoc, d₂₁_single_inv_mul_ρ_add_single, eq_d₂₁_comp_inv, d₂₁_single_inv_self_ρ_sub_self_inv, d₂₁_comp_d₁₀_apply, eq_d₂₁_comp_inv_assoc, d₂₁_comp_d₁₀, d₂₁_single_self_inv_ρ_sub_inv_self, d₂₁_apply_mem_cycles₁, shortComplexH2_g, d₂₁_single_one_fst, d₂₁_single_one_snd, d₃₂_comp_d₂₁, d₂₁_single, eq_d₂₁_comp_inv_apply, d₂₁_single_ρ_add_single_inv_mul, d₂₁_comp_d₁₀_assoc, d₃₂_comp_d₂₁_apply
d₃₂ 📖	CompOp	13 math math: d₃₂_single, eq_d₃₂_comp_inv, d₃₂_single_one_thd, d₃₂_comp_d₂₁_assoc, shortComplexH2_f, eq_d₃₂_comp_inv_apply, d₃₂_single_one_fst, eq_d₃₂_comp_inv_assoc, d₃₂_apply_mem_cycles₂, d₃₂_comp_d₂₁, d₃₂_single_one_snd, comp_d₃₂_eq, d₃₂_comp_d₂₁_apply
isoCycles₁ 📖	CompOp	16 math math: isoCycles₁_inv_comp_iCycles_apply, toCycles_comp_isoCycles₁_hom_apply, toCycles_comp_isoCycles₁_hom_assoc, π_comp_H1Iso_hom_apply, isoCycles₁_hom_comp_i_apply, cyclesMap_comp_isoCycles₁_hom_apply, isoCycles₁_inv_comp_iCycles_assoc, π_comp_H1Iso_hom_assoc, cyclesMk₁_eq, isoCycles₁_hom_comp_i_assoc, isoCycles₁_inv_comp_iCycles, cyclesMap_comp_isoCycles₁_hom_assoc, toCycles_comp_isoCycles₁_hom, π_comp_H1Iso_hom, isoCycles₁_hom_comp_i, cyclesMap_comp_isoCycles₁_hom
isoCycles₂ 📖	CompOp	16 math math: π_comp_H2Iso_hom_assoc, cyclesMap_comp_isoCycles₂_hom, toCycles_comp_isoCycles₂_hom_assoc, π_comp_H2Iso_hom, isoCycles₂_hom_comp_i_apply, cyclesMap_comp_isoCycles₂_hom_assoc, toCycles_comp_isoCycles₂_hom, cyclesMap_comp_isoCycles₂_hom_apply, toCycles_comp_isoCycles₂_hom_apply, isoCycles₂_inv_comp_iCycles_apply, isoCycles₂_inv_comp_iCycles_assoc, cyclesMk₂_eq, π_comp_H2Iso_hom_apply, isoCycles₂_hom_comp_i, isoCycles₂_inv_comp_iCycles, isoCycles₂_hom_comp_i_assoc
isoShortComplexH1 📖	CompOp	2 math math: isoShortComplexH1_hom, isoShortComplexH1_inv
isoShortComplexH2 📖	CompOp	2 math math: isoShortComplexH2_hom, isoShortComplexH2_inv
mkH1OfIsTrivial 📖	CompOp	2 math math: H1AddEquivOfIsTrivial_symm_apply, mkH1OfIsTrivial_apply
opcyclesIso₀ 📖	CompOp	6 math math: coinvariantsMk_comp_opcyclesIso₀_inv_assoc, pOpcycles_comp_opcyclesIso_hom_apply, coinvariantsMk_comp_opcyclesIso₀_inv_apply, pOpcycles_comp_opcyclesIso_hom, coinvariantsMk_comp_opcyclesIso₀_inv, pOpcycles_comp_opcyclesIso_hom_assoc
shortComplexH0 📖	CompOp	4 math math: shortComplexH0_f, shortComplexH0_exact, instEpiModuleCatGShortComplexH0, shortComplexH0_g
shortComplexH1 📖	CompOp	30 math math: shortComplexH1_f, mapShortComplexH1_zero, comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, π_comp_H1Iso_inv, isoCycles₁_inv_comp_iCycles_apply, mapShortComplexH1_τ₂, mapCycles₁_comp_i, toCycles_comp_isoCycles₁_hom_apply, mapCycles₁_comp_i_apply, isoShortComplexH1_hom, toCycles_comp_isoCycles₁_hom_assoc, mapShortComplexH1_id_comp, mapShortComplexH1_comp, π_comp_H1Iso_hom_apply, isoShortComplexH1_inv, isoCycles₁_hom_comp_i_apply, mapShortComplexH1_τ₁, isoCycles₁_inv_comp_iCycles_assoc, π_comp_H1Iso_hom_assoc, mapShortComplexH1_id, isoCycles₁_hom_comp_i_assoc, isoCycles₁_inv_comp_iCycles, toCycles_comp_isoCycles₁_hom, π_comp_H1Iso_hom, π_comp_H1Iso_inv_apply, isoCycles₁_hom_comp_i, mapShortComplexH1_τ₃, shortComplexH1_g, π_comp_H1Iso_inv_assoc, mapCycles₁_comp_i_assoc
shortComplexH2 📖	CompOp	29 math math: mapShortComplexH2_τ₁, π_comp_H2Iso_hom_assoc, mapShortComplexH2_id, mapShortComplexH2_zero, toCycles_comp_isoCycles₂_hom_assoc, π_comp_H2Iso_inv_assoc, shortComplexH2_f, mapCycles₂_comp_i, π_comp_H2Iso_hom, isoCycles₂_hom_comp_i_apply, mapShortComplexH2_comp, toCycles_comp_isoCycles₂_hom, mapShortComplexH2_τ₂, toCycles_comp_isoCycles₂_hom_apply, shortComplexH2_g, isoCycles₂_inv_comp_iCycles_apply, isoCycles₂_inv_comp_iCycles_assoc, isoShortComplexH2_hom, π_comp_H2Iso_inv, mapCycles₂_comp_i_assoc, π_comp_H2Iso_hom_apply, mapShortComplexH2_id_comp, isoShortComplexH2_inv, mapCycles₂_comp_i_apply, isoCycles₂_hom_comp_i, isoCycles₂_inv_comp_iCycles, mapShortComplexH2_τ₃, π_comp_H2Iso_inv_apply, isoCycles₂_hom_comp_i_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
H0IsoOfIsTrivial_inv_eq_π 📖	mathematical	—	CategoryTheory.Iso.inv ModuleCat CommRing.toRing ModuleCat.moduleCategory H0 Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0IsoOfIsTrivial H0π	—	—
H0_induction_on 📖	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid H0 ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H0π	—	—	groupHomology_induction_on cyclesIso₀_comp_H0π_apply
H0π_comp_H0Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0 CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor H0π CategoryTheory.Iso.hom H0Iso CategoryTheory.NatTrans.app Action Action.forget Rep.coinvariantsMk	—	CategoryTheory.Category.assoc π_comp_H0Iso_hom CategoryTheory.Iso.inv_hom_id_assoc
H0π_comp_H0Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier H0 Representation.Coinvariants Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom H0Iso H0π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise H0π_comp_H0Iso_hom
H0π_comp_H0Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0 H0π CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor CategoryTheory.Iso.hom H0Iso CategoryTheory.NatTrans.app Action Action.forget Rep.coinvariantsMk	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H0π_comp_H0Iso_hom
H1AddEquivOfIsTrivial_apply 📖	mathematical	—	DFunLike.coe AddEquiv ModuleCat.carrier CommRing.toRing H1 TensorProduct Int.instCommSemiring Additive Abelianization Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Additive.addCommMonoid CommGroup.toCommMonoid Abelianization.commGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toIntModule Additive.addCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ModuleCat.isAddCommGroup TensorProduct.add EquivLike.toFunLike AddEquiv.instEquivLike H1AddEquivOfIsTrivial LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.addCommGroup LinearMap.instFunLike H1ToTensorOfIsTrivial	—	—
H1AddEquivOfIsTrivial_single 📖	mathematical	—	DFunLike.coe AddEquiv ModuleCat.carrier CommRing.toRing H1 TensorProduct Int.instCommSemiring Additive Abelianization Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Additive.addCommMonoid CommGroup.toCommMonoid Abelianization.commGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toIntModule Additive.addCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ModuleCat.isAddCommGroup TensorProduct.add EquivLike.toFunLike AddEquiv.instEquivLike H1AddEquivOfIsTrivial ModuleCat.of Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π CategoryTheory.Iso.inv cycles₁IsoOfIsTrivial Finsupp.single TensorProduct.tmul Equiv Equiv.instEquivLike Additive.ofMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommGroup.toGroup MonoidHom.instFunLike Abelianization.of	—	H1AddEquivOfIsTrivial_apply H1ToTensorOfIsTrivial_H1π_single
H1AddEquivOfIsTrivial_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv TensorProduct Int.instCommSemiring Additive Abelianization ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Additive.addCommMonoid CommGroup.toCommMonoid Abelianization.commGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toIntModule Additive.addCommGroup H1 TensorProduct.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ModuleCat.isAddCommGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm H1AddEquivOfIsTrivial LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.addCommGroup LinearMap.instFunLike TensorProduct.lift mkH1OfIsTrivial	—	—
H1AddEquivOfIsTrivial_symm_tmul 📖	mathematical	—	DFunLike.coe AddEquiv TensorProduct Int.instCommSemiring Additive Abelianization ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Additive.addCommMonoid CommGroup.toCommMonoid Abelianization.commGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toIntModule Additive.addCommGroup H1 TensorProduct.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ModuleCat.isAddCommGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm H1AddEquivOfIsTrivial TensorProduct.tmul Equiv Equiv.instEquivLike Additive.ofMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommGroup.toGroup MonoidHom.instFunLike Abelianization.of ModuleCat.of Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π CategoryTheory.Iso.inv cycles₁IsoOfIsTrivial Finsupp.single	—	—
H1ToTensorOfIsTrivial_H1π_single 📖	mathematical	—	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing H1 TensorProduct Int.instCommSemiring Additive Abelianization Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Additive.addCommMonoid CommGroup.toCommMonoid Abelianization.commGroup AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toIntModule Additive.addCommGroup ModuleCat.isAddCommGroup TensorProduct.addCommMonoid TensorProduct.addCommGroup LinearMap.instFunLike H1ToTensorOfIsTrivial ModuleCat.of Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom Ring.toSemiring ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π CategoryTheory.Iso.inv cycles₁IsoOfIsTrivial Finsupp.single TensorProduct.tmul Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommGroup.toGroup MonoidHom.instFunLike Abelianization.of	—	AddSubgroup.normal_of_comm cycles₁_eq_top_of_isTrivial π_comp_H1Iso_hom_apply CategoryTheory.Iso.inv_hom_id_apply Finsupp.sum_single_index TensorProduct.tmul_zero
H1_induction_on 📖	—	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H1 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π	—	—	groupHomology_induction_on CategoryTheory.Iso.hom_inv_id_apply
H1π_eq_iff 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H1 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π boundaries₁ Finsupp.instSub	—	sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass H1π_eq_zero_iff
H1π_eq_zero_iff 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H1 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π boundaries₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc RingHomCompTriple.ids map_eq_zero_iff ModuleCat.mono_iff_injective AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv d₂₁_comp_d₁₀ LinearMap.range_codRestrict CategoryTheory.ShortComplex.moduleCat_zero_apply
H2_induction_on 📖	—	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H2 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H2π	—	—	groupHomology_induction_on CategoryTheory.Iso.hom_inv_id_apply
H2π_eq_iff 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H2 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H2π boundaries₂ Finsupp.instSub	—	sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass H2π_eq_zero_iff
H2π_eq_zero_iff 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H2 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H2π boundaries₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc RingHomCompTriple.ids map_eq_zero_iff ModuleCat.mono_iff_injective AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv d₃₂_comp_d₂₁ LinearMap.range_codRestrict CategoryTheory.ShortComplex.moduleCat_zero_apply
boundariesOfIsBoundary₁_coe 📖	mathematical	IsBoundary₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₁ boundariesOfIsBoundary₁	—	—
boundariesOfIsBoundary₂_coe 📖	mathematical	IsBoundary₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂ boundariesOfIsBoundary₂	—	—
boundariesToCycles₁_apply 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring boundaries₁ Submodule.addCommMonoid Submodule.module LinearMap.instFunLike boundariesToCycles₁	—	—
boundariesToCycles₂_apply 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring boundaries₂ Submodule.addCommMonoid Submodule.module LinearMap.instFunLike boundariesToCycles₂	—	—
boundaries₁_le_cycles₁ 📖	mathematical	—	Submodule Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder boundaries₁ cycles₁	—	mem_cycles₁_of_mem_boundaries₁
boundaries₂_le_cycles₂ 📖	mathematical	—	Submodule Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder boundaries₂ cycles₂	—	mem_cycles₂_of_mem_boundaries₂
chains₁ToCoinvariantsKer_surjective 📖	mathematical	—	ModuleCat.carrier CommRing.toRing ModuleCat.of Finsupp 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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring ModuleCat.isAddCommGroup SetLike.instMembership Submodule.setLike Representation.Coinvariants.ker Rep.ρ Submodule.addCommGroup Submodule.module DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier chains₁ToCoinvariantsKer	—	RingHomSurjective.ids range_d₁₀_eq_coinvariantsKer
coinvariantsKerOfIsBoundary₀_coe 📖	mathematical	IsBoundary₀ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Representation.Coinvariants.ker Representation.ofDistribMulAction coinvariantsKerOfIsBoundary₀	—	—
coinvariantsMk_comp_H0Iso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.forget Rep.coinvariantsFunctor H0 CategoryTheory.NatTrans.app Rep.coinvariantsMk CategoryTheory.Iso.inv Rep H0Iso H0π	—	CategoryTheory.CommSq.w CategoryTheory.CommSq.vert_inv π_comp_H0Iso_hom
coinvariantsMk_comp_H0Iso_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ H0 AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Action Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv Rep H0Iso H0π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise coinvariantsMk_comp_H0Iso_inv
coinvariantsMk_comp_H0Iso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.forget Rep.coinvariantsFunctor CategoryTheory.NatTrans.app Rep.coinvariantsMk H0 CategoryTheory.Iso.inv Rep H0Iso H0π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coinvariantsMk_comp_H0Iso_inv
coinvariantsMk_comp_opcyclesIso₀_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.forget Rep.coinvariantsFunctor HomologicalComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc CategoryTheory.NatTrans.app Rep.coinvariantsMk CategoryTheory.Iso.inv Rep opcyclesIso₀ Action.V HomologicalComplex.X chainsIso₀ HomologicalComplex.pOpcycles	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.CommSq.vert_inv pOpcycles_comp_opcyclesIso_hom
coinvariantsMk_comp_opcyclesIso₀_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Representation.Coinvariants ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ HomologicalComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Action Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv Rep opcyclesIso₀ Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module ModuleCat.of HomologicalComplex.pOpcycles chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise coinvariantsMk_comp_opcyclesIso₀_inv
coinvariantsMk_comp_opcyclesIso₀_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.forget Rep.coinvariantsFunctor CategoryTheory.NatTrans.app Rep.coinvariantsMk HomologicalComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc CategoryTheory.Iso.inv Rep opcyclesIso₀ HomologicalComplex.X Action.V chainsIso₀ HomologicalComplex.pOpcycles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coinvariantsMk_comp_opcyclesIso₀_inv
comp_d₁₀_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains 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 CategoryTheory.Iso.hom chainsIso₁ d₁₀ HomologicalComplex.d chainsIso₀	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.lhom_ext Finsupp.equivMapDomain_single d₁₀_single sub_eq_add_neg RingHomCompTriple.ids Fin.isEmpty' inhomogeneousChains.d_def inhomogeneousChains.d_single Unique.eq_default Finset.sum_congr Finset.univ_unique zero_add pow_one neg_smul one_smul Finset.sum_neg_distrib Finset.sum_const Finset.card_singleton Finsupp.single_eq_same
comp_d₂₁_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains 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 CategoryTheory.Iso.hom chainsIso₂ d₂₁ HomologicalComplex.d chainsIso₁	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.lhom_ext Finsupp.domLCongr_single d₂₁_single sub_eq_add_neg add_assoc RingHomCompTriple.ids inhomogeneousChains.d_def inhomogeneousChains.d_single Finset.sum_congr Finsupp.smul_single Fin.sum_univ_two zero_add pow_one neg_smul one_smul Finsupp.single_neg Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass RingHomInvPair.ids Nat.instZeroLEOneClass
comp_d₃₂_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains 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 CategoryTheory.Iso.hom chainsIso₃ d₃₂ HomologicalComplex.d chainsIso₂	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.lhom_ext RingHomCompTriple.ids LinearMap.comp.congr_simp sub_eq_add_neg add_assoc Finsupp.domLCongr_single Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero neg_zero add_zero add_rotate' add_left_comm inhomogeneousChains.d_def inhomogeneousChains.d_single Finset.sum_congr pow_succ mul_neg mul_one neg_smul Finsupp.smul_single Finset.sum_neg_distrib Fin.sum_univ_three pow_zero one_smul Finsupp.single_neg neg_neg neg_add_rev map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_neg RingHomInvPair.ids IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instCanonicallyOrderedAdd
cyclesIso₀_comp_H0π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0 CategoryTheory.Iso.hom cyclesIso₀ H0π π	—	CategoryTheory.Iso.hom_inv_id_assoc
cyclesIso₀_comp_H0π_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid H0 AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier H0π cycles CategoryTheory.Iso.hom cyclesIso₀ π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cyclesIso₀_comp_H0π
cyclesIso₀_comp_H0π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.hom cyclesIso₀ H0 H0π π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso₀_comp_H0π
cyclesIso₀_inv_comp_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid cycles 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 inhomogeneousChains CategoryTheory.Iso.inv cyclesIso₀ iCycles chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc HomologicalComplex.iCyclesIso_inv_hom_id CategoryTheory.Category.comp_id
cyclesIso₀_inv_comp_iCycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommGroup ModuleCat.isModule Finsupp.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of iCycles CategoryTheory.Iso.inv cyclesIso₀ chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cyclesIso₀_inv_comp_iCycles
cyclesIso₀_inv_comp_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid cycles CategoryTheory.Iso.inv cyclesIso₀ 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 inhomogeneousChains iCycles chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso₀_inv_comp_iCycles
cyclesMk₀_eq 📖	mathematical	—	cyclesMk DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid 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 inhomogeneousChains ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv chainsIso₀ cycles cyclesIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.mono_iff_injective HomologicalComplex.instMonoICycles cyclesIso₀_inv_comp_iCycles_apply
cyclesMk₁_eq 📖	mathematical	—	cyclesMk 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 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 inhomogeneousChains CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv chainsIso₁ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Submodule.module cycles isoCycles₁	—	AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.mono_iff_injective HomologicalComplex.instMonoICycles isoCycles₁_inv_comp_iCycles_apply
cyclesMk₂_eq 📖	mathematical	—	cyclesMk 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 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 inhomogeneousChains CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv chainsIso₂ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Submodule.module cycles isoCycles₂	—	AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.mono_iff_injective HomologicalComplex.instMonoICycles isoCycles₂_inv_comp_iCycles_apply
cyclesOfIsCycle₁_coe 📖	mathematical	IsCycle₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ cyclesOfIsCycle₁	—	—
cyclesOfIsCycle₂_coe 📖	mathematical	IsCycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ cyclesOfIsCycle₂	—	—
cycles₁IsoOfIsTrivial_hom_apply 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module Ring.toSemiring CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom cycles₁IsoOfIsTrivial	—	—
cycles₁IsoOfIsTrivial_inv_apply 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ DFunLike.coe ModuleCat.of Finsupp.instAddCommGroup Ring.toSemiring Submodule.addCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv cycles₁IsoOfIsTrivial	—	—
cycles₁_eq_top_of_isTrivial 📖	mathematical	—	cycles₁ Top.top Submodule Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule Submodule.instTop	—	cycles₁.eq_1 d₁₀_eq_zero_of_isTrivial ModuleCat.hom_zero LinearMap.ker_zero
d₁₀ArrowIso_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousChains HomologicalComplex.d 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₁₀ CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd d₁₀ArrowIso chainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
d₁₀ArrowIso_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousChains HomologicalComplex.d 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₁₀ CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd d₁₀ArrowIso chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
d₁₀ArrowIso_inv_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id 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₁₀ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousChains HomologicalComplex.d CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd d₁₀ArrowIso chainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
d₁₀ArrowIso_inv_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id 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₁₀ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousChains HomologicalComplex.d CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd d₁₀ArrowIso chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
d₁₀_comp_coinvariantsMk 📖	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 CategoryTheory.Functor.obj Action Action.instCategory Rep.coinvariantsFunctor d₁₀ CategoryTheory.NatTrans.app Action.forget Rep.coinvariantsMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	ModuleCat.hom_ext Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_self map_sub Representation.Coinvariants.mk_self_apply
d₁₀_comp_coinvariantsMk_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Representation.Coinvariants ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Action Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of d₁₀ LinearMap.instZero	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise d₁₀_comp_coinvariantsMk
d₁₀_comp_coinvariantsMk_assoc 📖	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₁₀ CategoryTheory.Functor.obj Action Action.instCategory Rep.coinvariantsFunctor CategoryTheory.NatTrans.app Action.forget Rep.coinvariantsMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₁₀_comp_coinvariantsMk
d₁₀_eq_zero_of_isTrivial 📖	mathematical	—	d₁₀ Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver 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 ModuleCat.instZeroHom	—	ModuleCat.hom_ext Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids LinearMap.comp.congr_simp Representation.isTrivial_def sub_self Finsupp.lsum_comp_lsingle
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 SubNegMonoid.toSub 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	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_self
d₁₀_single_inv 📖	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 InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NegZeroClass.toNeg CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	Finsupp.sum_single_index inv_inv map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_self Representation.inv_self_apply neg_sub
d₁₀_single_one 📖	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 InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finsupp.sum_single_index inv_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass sub_self
d₂₁_apply_mem_cycles₁ 📖	mathematical	—	ModuleCat.carrier CommRing.toRing ModuleCat.of Finsupp 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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid SetLike.instMembership Submodule.setLike cycles₁ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₂₁	—	d₂₁_comp_d₁₀
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₂₁ d₁₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	ModuleCat.hom_ext Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self add_zero Finsupp.sum_add_index' map_add SemilinearMapClass.toAddHomClass add_sub_add_comm Finsupp.sum_sub_index map_sub sub_sub_sub_comm mul_inv_rev map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass sub_sub_sub_cancel_left sub_add_sub_cancel
d₂₁_comp_d₁₀_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup ModuleCat.isAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of d₁₀ d₂₁ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise d₂₁_comp_d₁₀
d₂₁_comp_d₁₀_assoc 📖	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₂₁ d₁₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₂₁_comp_d₁₀
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 Finsupp.instSub 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 MulOne.toMul	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self add_zero
d₂₁_single_inv_mul_ρ_add_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.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finsupp.single InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass d₂₁_single inv_inv Representation.self_inv_apply inv_mul_cancel_left Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg
d₂₁_single_inv_self_ρ_sub_self_inv 📖	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.instSub Finsupp.single InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toOne	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass d₂₁_single inv_inv Representation.self_inv_apply inv_mul_cancel mul_inv_cancel Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
d₂₁_single_one_fst 📖	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 InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finsupp.sum_single_index LinearMap.comp.congr_simp inv_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul Finsupp.single_zero sub_self add_zero zero_add
d₂₁_single_one_snd 📖	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 InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv	—	Finsupp.sum_single_index mul_one sub_add_cancel map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero
d₂₁_single_self_inv_ρ_sub_inv_self 📖	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.instSub Finsupp.single InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toOne	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass d₂₁_single Representation.inv_self_apply mul_inv_cancel inv_inv inv_mul_cancel Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
d₂₁_single_ρ_add_single_inv_mul 📖	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.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finsupp.single 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 MulOne.toMul	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass d₂₁_single Representation.inv_self_apply inv_inv inv_mul_cancel_left Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg
d₃₂_apply_mem_cycles₂ 📖	mathematical	—	ModuleCat.carrier CommRing.toRing ModuleCat.of Finsupp 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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid SetLike.instMembership Submodule.setLike cycles₂ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₃₂	—	d₃₂_comp_d₂₁
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₃₂ d₂₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc HomologicalComplex.d_comp_d CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
d₃₂_comp_d₂₁_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of d₂₁ d₃₂ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise d₃₂_comp_d₂₁
d₃₂_comp_d₂₁_assoc 📖	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₃₂ d₂₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₃₂_comp_d₂₁
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.instSub 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 MulOne.toMul	—	LinearMap.comp.congr_simp Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self add_zero
d₃₂_single_one_fst 📖	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 InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Finsupp.instSub MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	LinearMap.comp.congr_simp Finsupp.sum_single_index inv_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul Finsupp.single_zero sub_self add_zero zero_add
d₃₂_single_one_snd 📖	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 InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Finsupp.instSub CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv	—	LinearMap.comp.congr_simp Finsupp.sum_single_index mul_one one_mul sub_add_cancel map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self
d₃₂_single_one_thd 📖	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 InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Finsupp.instSub CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv MulOne.toMul	—	LinearMap.comp.congr_simp Finsupp.sum_single_index mul_one add_sub_cancel_right map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self
eq_d₁₀_comp_inv 📖	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 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 inhomogeneousChains CategoryTheory.Iso.inv chainsIso₁ HomologicalComplex.d d₁₀ chainsIso₀	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv comp_d₁₀_eq
eq_d₁₀_comp_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains CategoryTheory.Iso.inv chainsIso₁ chainsIso₀ d₁₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise eq_d₁₀_comp_inv
eq_d₁₀_comp_inv_assoc 📖	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 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 inhomogeneousChains CategoryTheory.Iso.inv chainsIso₁ HomologicalComplex.d d₁₀ chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eq_d₁₀_comp_inv
eq_d₂₁_comp_inv 📖	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 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 inhomogeneousChains CategoryTheory.Iso.inv chainsIso₂ HomologicalComplex.d d₂₁ chainsIso₁	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv comp_d₂₁_eq
eq_d₂₁_comp_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains CategoryTheory.Iso.inv chainsIso₂ chainsIso₁ d₂₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise eq_d₂₁_comp_inv
eq_d₂₁_comp_inv_assoc 📖	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 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 inhomogeneousChains CategoryTheory.Iso.inv chainsIso₂ HomologicalComplex.d d₂₁ chainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eq_d₂₁_comp_inv
eq_d₃₂_comp_inv 📖	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 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 inhomogeneousChains CategoryTheory.Iso.inv chainsIso₃ HomologicalComplex.d d₃₂ chainsIso₂	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv comp_d₃₂_eq
eq_d₃₂_comp_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains CategoryTheory.Iso.inv chainsIso₃ chainsIso₂ d₃₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise eq_d₃₂_comp_inv
eq_d₃₂_comp_inv_assoc 📖	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 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 inhomogeneousChains CategoryTheory.Iso.inv chainsIso₃ HomologicalComplex.d d₃₂ chainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eq_d₃₂_comp_inv
instEpiModuleCatGShortComplexH0 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	Rep.instEpiModuleCatAppActionCoinvariantsMk
instEpiModuleCatH0π 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0 H0π	—	CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv HomologicalComplex.instEpiHomologyπ
instEpiModuleCatH1π 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing 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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H1 H1π	—	CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv HomologicalComplex.instEpiHomologyπ
instEpiModuleCatH2π 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing 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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module H2 H2π	—	CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv HomologicalComplex.instEpiHomologyπ
isBoundary₀_iff 📖	mathematical	—	IsBoundary₀ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.sum NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.toAddCommMonoid SubNegMonoid.toSub	—	Finsupp.single_neg Finsupp.sum_neg Finsupp.sum_sub Finsupp.sum_neg_index smul_zero smul_neg Finsupp.sum_sum_index smul_add Finsupp.sum_single_index smul_inv_smul sub_neg_eq_add neg_add_eq_sub inv_smul_smul
isBoundary₀_of_mem_coinvariantsKer 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Representation.Coinvariants.ker DivInvMonoid.toMonoid Group.toDivInvMonoid Representation.ofDistribMulAction	IsBoundary₀ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Submodule.span_induction Finsupp.sum_sub Finsupp.sum_single_index inv_inv smul_zero sub_self Finsupp.sum_add_index' smul_add add_sub_add_comm Finsupp.sum_smul_index' SMulCommClass.smul_comm smul_sub Finsupp.smul_sum
isBoundary₁_iff 📖	mathematical	—	IsBoundary₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Finsupp.sum Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.instAdd Finsupp.instSub Finsupp.single	—	Finsupp.sum_add Finsupp.sum_sub Finsupp.sum_sum_index Finsupp.single_zero Finsupp.single_add Finsupp.sum_single_index smul_zero smul_add smul_inv_smul inv_smul_smul
isBoundary₁_of_mem_boundaries₁ 📖	mathematical	Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₁	IsBoundary₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
isBoundary₂_iff 📖	mathematical	—	IsBoundary₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Finsupp.sum Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.instSub Finsupp.instAdd Finsupp.single	—	Finsupp.sum_sub Finsupp.sum_add Finsupp.sum_sum_index Finsupp.single_zero Finsupp.single_add Finsupp.sum_single_index smul_zero smul_add smul_inv_smul inv_smul_smul
isBoundary₂_of_mem_boundaries₂ 📖	mathematical	Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂	IsBoundary₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
isCycle₁_of_mem_cycles₁ 📖	mathematical	Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁	IsCycle₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_cycles₁_iff
isCycle₂_of_mem_cycles₂ 📖	mathematical	Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂	IsCycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_cycles₂_iff
isoCycles₁_hom_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.Iso.hom isoCycles₁ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains Ring.toSemiring iCycles chainsIso₁	—	comp_d₂₁_eq comp_d₁₀_eq CategoryTheory.ShortComplex.cyclesMap'_i CategoryTheory.Category.id_comp
isoCycles₁_hom_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule.addCommGroup Finsupp.instAddCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g cycles CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCycles₁ chainsIso₁ iCycles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCycles₁_hom_comp_i
isoCycles₁_hom_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.Iso.hom isoCycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains iCycles Ring.toSemiring chainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCycles₁_hom_comp_i
isoCycles₁_inv_comp_iCycles 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module cycles 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 inhomogeneousChains CategoryTheory.Iso.inv isoCycles₁ iCycles CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i Ring.toSemiring chainsIso₁	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv isoCycles₁_hom_comp_i
isoCycles₁_inv_comp_iCycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommGroup ModuleCat.isModule Finsupp.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of iCycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv isoCycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 chainsIso₁ Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCycles₁_inv_comp_iCycles
isoCycles₁_inv_comp_iCycles_assoc 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module cycles CategoryTheory.Iso.inv isoCycles₁ 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 inhomogeneousChains iCycles CategoryTheory.ShortComplex.X₂ shortComplexH1 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData Ring.toSemiring chainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCycles₁_inv_comp_iCycles
isoCycles₂_hom_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.Iso.hom isoCycles₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains Ring.toSemiring iCycles chainsIso₂	—	comp_d₃₂_eq comp_d₂₁_eq CategoryTheory.ShortComplex.cyclesMap'_i CategoryTheory.Category.id_comp
isoCycles₂_hom_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule.addCommGroup Finsupp.instAddCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g cycles CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCycles₂ chainsIso₂ iCycles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCycles₂_hom_comp_i
isoCycles₂_hom_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.Iso.hom isoCycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains iCycles Ring.toSemiring chainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCycles₂_hom_comp_i
isoCycles₂_inv_comp_iCycles 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module cycles 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 inhomogeneousChains CategoryTheory.Iso.inv isoCycles₂ iCycles CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i Ring.toSemiring chainsIso₂	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv isoCycles₂_hom_comp_i
isoCycles₂_inv_comp_iCycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommGroup ModuleCat.isModule Finsupp.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of iCycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv isoCycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 chainsIso₂ Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCycles₂_inv_comp_iCycles
isoCycles₂_inv_comp_iCycles_assoc 📖	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 Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module cycles CategoryTheory.Iso.inv isoCycles₂ 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 inhomogeneousChains iCycles CategoryTheory.ShortComplex.X₂ shortComplexH2 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData Ring.toSemiring chainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCycles₂_inv_comp_iCycles
isoShortComplexH1_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains shortComplexH1 isoShortComplexH1 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc' CategoryTheory.ShortComplex.isoMk chainsIso₂ chainsIso₁ chainsIso₀ comp_d₂₁_eq comp_d₁₀_eq	—	AddRightCancelSemigroup.toIsRightCancelAdd
isoShortComplexH1_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains shortComplexH1 isoShortComplexH1 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.ShortComplex.homMk 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 CategoryTheory.ShortComplex.X₁ chainsIso₂ CategoryTheory.ShortComplex.X₂ chainsIso₁ CategoryTheory.ShortComplex.X₃ chainsIso₀ comp_d₂₁_eq comp_d₁₀_eq CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor' HomologicalComplex.shortComplexFunctor CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc'	—	AddRightCancelSemigroup.toIsRightCancelAdd
isoShortComplexH2_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains shortComplexH2 isoShortComplexH2 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc' CategoryTheory.ShortComplex.isoMk chainsIso₃ chainsIso₂ chainsIso₁ comp_d₃₂_eq comp_d₂₁_eq	—	AddRightCancelSemigroup.toIsRightCancelAdd
isoShortComplexH2_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousChains shortComplexH2 isoShortComplexH2 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.ShortComplex.homMk 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 CategoryTheory.ShortComplex.X₁ chainsIso₃ CategoryTheory.ShortComplex.X₂ chainsIso₂ CategoryTheory.ShortComplex.X₃ chainsIso₁ comp_d₃₂_eq comp_d₂₁_eq CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor' HomologicalComplex.shortComplexFunctor CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc'	—	AddRightCancelSemigroup.toIsRightCancelAdd
mem_cycles₁_iff 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Finsupp.sum DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finsupp.sum_sub sub_eq_zero
mem_cycles₁_of_mem_boundaries₁ 📖	mathematical	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₁	cycles₁	—	d₂₁_apply_mem_cycles₁
mem_cycles₂_iff 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Finsupp.sum Finsupp.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finsupp.single DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul	—	sub_add_eq_add_sub Finsupp.sum_sub Finsupp.sum_add
mem_cycles₂_of_mem_boundaries₂ 📖	mathematical	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂	cycles₂	—	d₃₂_apply_mem_cycles₂
mkH1OfIsTrivial_apply 📖	mathematical	—	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid H1 AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isAddCommGroup AddCommGroup.toIntModule LinearMap.instFunLike Additive Abelianization Additive.addCommMonoid CommGroup.toCommMonoid Abelianization.commGroup LinearMap.addCommMonoid Additive.addCommGroup LinearMap.addCommGroup mkH1OfIsTrivial Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommGroup.toGroup MonoidHom.instFunLike Abelianization.of ModuleCat.of Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.ConcreteCategory.hom Ring.toSemiring ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π CategoryTheory.Iso.inv cycles₁IsoOfIsTrivial Finsupp.single	—	—
pOpcycles_comp_opcyclesIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains HomologicalComplex.opcycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Rep.coinvariantsFunctor HomologicalComplex.pOpcycles CategoryTheory.Iso.hom opcyclesIso₀ Action.V Action chainsIso₀ CategoryTheory.NatTrans.app Action.forget Rep.coinvariantsMk	—	CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.d_pOpcycles
pOpcycles_comp_opcyclesIso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier HomologicalComplex.opcycles ModuleCat 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 inhomogeneousChains CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc Representation.Coinvariants Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom opcyclesIso₀ Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Finsupp.instAddCommGroup Finsupp.module ModuleCat.of HomologicalComplex.pOpcycles chainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise pOpcycles_comp_opcyclesIso_hom
pOpcycles_comp_opcyclesIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains HomologicalComplex.opcycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc HomologicalComplex.pOpcycles CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Rep.coinvariantsFunctor CategoryTheory.Iso.hom opcyclesIso₀ Action.V chainsIso₀ CategoryTheory.NatTrans.app Action Action.forget Rep.coinvariantsMk	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_comp_opcyclesIso_hom
range_d₁₀_eq_coinvariantsKer 📖	mathematical	—	LinearMap.range ModuleCat.carrier CommRing.toRing ModuleCat.of Finsupp 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 ModuleCat.isAddCommGroup RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom d₁₀ Representation.Coinvariants.ker Rep.ρ	—	RingHomSurjective.ids Submodule.span_eq_of_le Finsupp.sum_single_index inv_inv map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_self Finsupp.induction AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass map_add SemilinearMapClass.toAddHomClass d₁₀_single Submodule.add_mem Representation.Coinvariants.mem_ker_of_eq
shortComplexH0_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0	—	CategoryTheory.ShortComplex.moduleCat_exact_iff RingHomSurjective.ids range_d₁₀_eq_coinvariantsKer Representation.Coinvariants.mk_eq_zero
shortComplexH0_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 d₁₀	—	—
shortComplexH0_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.NatTrans.app Action DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.forget Rep.coinvariantsFunctor Rep.coinvariantsMk	—	—
shortComplexH1_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 d₂₁	—	—
shortComplexH1_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 d₁₀	—	—
shortComplexH2_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 d₃₂	—	—
shortComplexH2_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 d₂₁	—	—
single_inv_ρ_self_add_single_mem_boundaries₁ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₁ Finsupp.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finsupp.single InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	d₂₁_single_inv_mul_ρ_add_single Set.mem_range_self
single_isCycle₁_iff 📖	mathematical	—	IsCycle₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	MulAction.bijective Finsupp.sum_single_index smul_zero inv_smul_smul
single_isCycle₁_of_mem_fixedPoints 📖	mathematical	Set Set.instMembership MulAction.fixedPoints DivInvMonoid.toMonoid Group.toDivInvMonoid DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	IsCycle₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Finsupp.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Finsupp.sum_single_index smul_zero
single_isCycle₂_iff 📖	mathematical	—	IsCycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Finsupp.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp Finsupp.instAdd	—	smul_zero Finsupp.mapRange_injective MulAction.bijective Finsupp.sum_add Finsupp.sum_single_index Finsupp.single_zero Finsupp.mapRange_add smul_add Finsupp.mapRange_single inv_smul_smul
single_isCycle₂_iff_inv 📖	mathematical	—	IsCycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Finsupp.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp Finsupp.instAdd	—	Finsupp.sum_add Finsupp.sum_single_index smul_zero Finsupp.single_zero
single_mem_cycles₁_iff 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Finsupp.single DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Representation.apply_bijective Representation.self_inv_apply
single_mem_cycles₁_of_mem_invariants 📖	mathematical	ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ	Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommMonoid Finsupp.module cycles₁ Finsupp.single	—	single_mem_cycles₁_iff
single_mem_cycles₂_iff 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Finsupp.single MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Finsupp.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.mapRange_injective Representation.apply_bijective Finsupp.sum_add Finsupp.sum_single_index Finsupp.single_zero Finsupp.mapRange_single Representation.inv_self_apply Finsupp.mapRange_add map_add SemilinearMapClass.toAddHomClass
single_mem_cycles₂_iff_inv 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Finsupp.single Finsupp.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul	—	Finsupp.sum_add Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero
single_one_fst_sub_single_one_fst_mem_boundaries₂ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂ Finsupp.instSub Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	LinearMap.comp.congr_simp Finsupp.sum_single_index inv_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul Finsupp.single_zero sub_self add_zero zero_add
single_one_fst_sub_single_one_snd_mem_boundaries₂ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂ Finsupp.instSub Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv	—	LinearMap.comp.congr_simp Finsupp.sum_single_index mul_one one_mul sub_add_cancel map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self
single_one_mem_boundaries₁ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₁ Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finsupp.sum_single_index LinearMap.comp.congr_simp inv_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one sub_add_cancel Finsupp.single_zero
single_one_snd_sub_single_one_fst_mem_boundaries₂ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂ Finsupp.instSub Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_neg d₃₂_single Representation.inv_self_apply mul_one one_mul sub_add_cancel neg_sub
single_one_snd_sub_single_one_snd_mem_boundaries₂ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₂ Finsupp.instSub Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv MulOne.toMul	—	LinearMap.comp.congr_simp Finsupp.sum_single_index mul_one add_sub_cancel_right map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero sub_self
single_ρ_self_add_single_inv_mem_boundaries₁ 📖	mathematical	—	Finsupp ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike boundaries₁ Finsupp.instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finsupp.single DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	d₂₁_single_ρ_add_single_inv_mul Set.mem_range_self
toCycles_comp_isoCycles₁_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module toCycles CategoryTheory.Iso.hom isoCycles₁ Ring.toSemiring CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData chainsIso₂ CategoryTheory.ShortComplex.LeftHomologyData.f'	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc isoCycles₁_hom_comp_i HomologicalComplex.toCycles_i_assoc CategoryTheory.ShortComplex.LeftHomologyData.f'_i comp_d₂₁_eq
toCycles_comp_isoCycles₁_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ ModuleCat.isAddCommGroup Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCycles₁ toCycles CategoryTheory.ShortComplex.moduleCatToCycles shortComplexH1 chainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toCycles_comp_isoCycles₁_hom
toCycles_comp_isoCycles₁_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains cycles toCycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.Iso.hom isoCycles₁ Ring.toSemiring chainsIso₂ CategoryTheory.ShortComplex.LeftHomologyData.f' shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_comp_isoCycles₁_hom
toCycles_comp_isoCycles₂_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains cycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module toCycles CategoryTheory.Iso.hom isoCycles₂ Ring.toSemiring CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData chainsIso₃ CategoryTheory.ShortComplex.LeftHomologyData.f'	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc isoCycles₂_hom_comp_i HomologicalComplex.toCycles_i_assoc CategoryTheory.ShortComplex.LeftHomologyData.f'_i comp_d₃₂_eq
toCycles_comp_isoCycles₂_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cycles Finsupp Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ ModuleCat.isAddCommGroup Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCycles₂ toCycles CategoryTheory.ShortComplex.moduleCatToCycles shortComplexH2 chainsIso₃	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toCycles_comp_isoCycles₂_hom
toCycles_comp_isoCycles₂_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory 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 inhomogeneousChains cycles toCycles ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module CategoryTheory.Iso.hom isoCycles₂ Ring.toSemiring chainsIso₃ CategoryTheory.ShortComplex.LeftHomologyData.f' shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_comp_isoCycles₂_hom
π_comp_H0IsoOfIsTrivial_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid π CategoryTheory.Iso.hom H0 H0IsoOfIsTrivial cyclesIso₀	—	HomologicalComplex.isoHomologyπ_hom_inv_id_assoc
π_comp_H0IsoOfIsTrivial_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupHomology Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom H0 H0IsoOfIsTrivial cycles π cyclesIso₀	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H0IsoOfIsTrivial_hom
π_comp_H0IsoOfIsTrivial_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology π Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.hom H0 H0IsoOfIsTrivial cyclesIso₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H0IsoOfIsTrivial_hom
π_comp_H0Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Rep.coinvariantsFunctor π CategoryTheory.Iso.hom H0 H0Iso Action.V Action cyclesIso₀ CategoryTheory.NatTrans.app Action.forget Rep.coinvariantsMk	—	HomologicalComplex.homology_π_ι_assoc pOpcycles_comp_opcyclesIso_hom CategoryTheory.Category.assoc
π_comp_H0Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupHomology Representation.Coinvariants Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Rep.ρ AddCommGroup.toAddCommMonoid CategoryTheory.Functor.obj Rep Action.instCategory Rep.coinvariantsFunctor LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom H0 H0Iso cycles π cyclesIso₀	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H0Iso_hom
π_comp_H0Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology π CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Rep.coinvariantsFunctor CategoryTheory.Iso.hom H0 H0Iso Action.V cyclesIso₀ CategoryTheory.NatTrans.app Action Action.forget Rep.coinvariantsMk	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H0Iso_hom
π_comp_H1Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData π CategoryTheory.Iso.hom H1 H1Iso ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module isoCycles₁ CategoryTheory.ShortComplex.LeftHomologyData.π	—	comp_d₂₁_eq comp_d₁₀_eq CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc CategoryTheory.ShortComplex.leftHomologyπ_naturality'
π_comp_H1Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupHomology HasQuotient.Quotient CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H1 H1Iso cycles π Finsupp Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module cycles₁ Finsupp.instAddCommGroup Submodule.mkQ isoCycles₁	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H1Iso_hom
π_comp_H1Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology π CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.Iso.hom H1 H1Iso ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₁ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module isoCycles₁ CategoryTheory.ShortComplex.LeftHomologyData.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H1Iso_hom
π_comp_H1Iso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.H H1 CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.Iso.inv H1Iso H1π	—	CategoryTheory.CommSq.w CategoryTheory.CommSq.vert_inv π_comp_H1Iso_hom
π_comp_H1Iso_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient ModuleCat.carrier CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.moduleCatToCycles H1 Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.inv H1Iso H1π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H1Iso_inv
π_comp_H1Iso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.π H1 CategoryTheory.Iso.inv H1Iso H1π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H1Iso_inv
π_comp_H2Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData π CategoryTheory.Iso.hom H2 H2Iso ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module isoCycles₂ CategoryTheory.ShortComplex.LeftHomologyData.π	—	comp_d₃₂_eq comp_d₂₁_eq CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc CategoryTheory.ShortComplex.leftHomologyπ_naturality'
π_comp_H2Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupHomology HasQuotient.Quotient CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H2 H2Iso cycles π Finsupp Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid Finsupp.module cycles₂ Finsupp.instAddCommGroup Submodule.mkQ isoCycles₂	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H2Iso_hom
π_comp_H2Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cycles groupHomology π CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.Iso.hom H2 H2Iso ModuleCat.of Finsupp ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cycles₂ Submodule.addCommGroup Finsupp.instAddCommGroup Submodule.module isoCycles₂ CategoryTheory.ShortComplex.LeftHomologyData.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H2Iso_hom
π_comp_H2Iso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.H H2 CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.Iso.inv H2Iso H2π	—	CategoryTheory.CommSq.w CategoryTheory.CommSq.vert_inv π_comp_H2Iso_hom
π_comp_H2Iso_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient ModuleCat.carrier CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.moduleCatToCycles H2 Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.inv H2Iso H2π	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H2Iso_inv
π_comp_H2Iso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.π H2 CategoryTheory.Iso.inv H2Iso H2π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H2Iso_inv

---

← Back to Index