Basic

📁 Source: Mathlib/RepresentationTheory/Rep/Basic.lean

Statistics

Metric	Count
Definitions Rep, ActionToRep, ActionToRep_RepToAction, hom, hom, hom', toModuleCatHom, IsTrivial, linearHomEquiv, linearHomEquivComm, RepToAction, RepToAction_ActionToRep, V, applyAsHom, diagonal, diagonalOneIsoLeftRegular, finsupp, finsuppTensorLeft, finsuppTensorRight, forgetNatIsoActionForget, free, freeLift, freeLiftLEquiv, hV1, hV2, hasForgetToModuleCat, homEquiv, homLinearEquiv, ihom, instAddCommGroupHom, instAddHom, instBraidedCategory, instCategory, instCoeSortType, instConcreteCategoryIntertwiningMapVρ, instInhabited, instLinear, instModuleHom, instMonoidalActionTypeLinearization, instMonoidalCategory, instMonoidalClosed, instNegHom, instPreadditive, instSMulHom, instSMulIntHom, instSMulNatHom, instSubHom, instSymmetricCategory, instZeroHom, leftRegular, leftRegularHom, leftRegularHomEquiv, leftRegularTensorTrivialIsoFree, linearization, linearizationOfMulActionIso, linearizationTrivialIso, mkIso, mkQ, norm, normNatTrans, of, ofAlgebraAut, ofAlgebraAutOnUnits, ofDistribMulAction, ofHom, ofMulAction, ofMulActionSubsingletonIsoTrivial, ofMulDistribMulAction, quotient, repIsoAction, subrepresentation, subtype, tensorHomEquiv, trivial, trivialFunctor, ρ, equivOfIso	77
Theorems ActionToRep_map, ActionToRep_obj_V, ActionToRep_obj_ρ, ext, ext_iff, linearHomEquivComm_hom, linearHomEquivComm_symm_hom, linearHomEquiv_hom, linearHomEquiv_symm_hom, RepToAction_map_hom, RepToAction_obj, RepToAction_obj_V_carrier, RepToAction_obj_V_isAddCommGroup, RepToAction_obj_V_isModule, RepToAction_obj_ρ, add_comp, add_hom, applyAsHom_apply, applyAsHom_comm, applyAsHom_comm_apply, applyAsHom_comm_assoc, comp_add, comp_apply, comp_smul, epi_iff_surjective, finsupp_V, forget_map, forget_obj, forget₂_moduleCat_map, forget₂_moduleCat_obj, free_ext, homEquiv_apply, homEquiv_def, homEquiv_symm_apply, hom_bijective, hom_braiding, hom_comm_apply, hom_comp, hom_comp_toLinearMap, hom_ext, hom_ext_iff, hom_hom_associator, hom_hom_leftUnitor, hom_hom_rightUnitor, hom_id, hom_injective, hom_inv_apply, hom_inv_associator, hom_inv_leftUnitor, hom_inv_rightUnitor, hom_ofHom, hom_surjective, hom_tensorHom, hom_whiskerLeft, hom_whiskerRight, id_apply, ihom_coev_app_hom, ihom_ev_app_hom, ihom_map, ihom_obj_V, ihom_obj_ρ, ihom_obj_ρ_apply, ihom_obj_ρ_def, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, instEpiModuleCatToModuleCatHom, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, instIsEquivalenceActionModuleCatActionToRep, instIsEquivalenceActionModuleCatRepToAction, instIsTrivialObjModuleCatTrivialFunctor, instIsTrivialOfOfIsTrivial, instIsTrivialTrivial, instIsTrivialVOfCompLinearMapIdρ, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, instMonoModuleCatToModuleCatHom, instMonoidalLinear, instMonoidalPreadditive, inv_hom_apply, leftRegularHomEquiv_symm_single, leftRegularHom_hom_single, linearization_map, linearization_obj_V, linearization_obj_ρ, mkIso_hom_hom, mkIso_hom_hom_apply, mkIso_hom_hom_toLinearMap, mkIso_inv_hom_apply, mkIso_inv_hom_toLinearMap, mkQ_hom_toFun, mono_iff_injective, neg_hom, normNatTrans_app, norm_apply, norm_comm, norm_comm_apply, norm_comm_assoc, nsmul_hom, ofDistribMulAction_ρ_apply_apply, ofHom_add, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofHom_neg, ofHom_nsmul, ofHom_smul, ofHom_sub, ofHom_sum, ofHom_zero, ofHom_zsmul, ofMulDistribMulAction_ρ_apply_apply, of_V, of_tensor, of_ρ, preservesColimits_forget, preservesLimits_forget, reflectsIsomorphisms_forget, smul_comp, smul_hom, sub_hom, subtype_hom_toFun, sum_hom, tensorHomEquiv_apply, tensorHomEquiv_symm_apply, tensorUnit_V, tensorUnit_ρ, tensor_V, tensor_ρ, toAdditive_apply, toAdditive_symm_apply, trivialFunctor_map_hom, trivialFunctor_obj_V, trivial_V, trivial_ρ, trivial_ρ_apply, zero_hom, zsmul_hom, δ_def, δ_hom, ε_def, ε_hom, η_def, η_hom, μ_def, μ_hom, ρ_mul, equivOfIso_invFun, equivOfIso_toFun	147
Total	224

Rep

Definitions

Name	Category	Theorems
ActionToRep 📖	CompOp	4 math math: ActionToRep_obj_ρ, ActionToRep_obj_V, ActionToRep_map, instIsEquivalenceActionModuleCatActionToRep
ActionToRep_RepToAction 📖	CompOp	—
IsTrivial 📖	MathDef	3 math math: instIsTrivialObjModuleCatTrivialFunctor, instIsTrivialTrivial, instIsTrivialOfOfIsTrivial
RepToAction 📖	CompOp	7 math math: RepToAction_map_hom, RepToAction_obj_V_isAddCommGroup, RepToAction_obj_V_carrier, RepToAction_obj_V_isModule, instIsEquivalenceActionModuleCatRepToAction, RepToAction_obj_ρ, RepToAction_obj
RepToAction_ActionToRep 📖	CompOp	—
V 📖	CompOp	575 math math: groupCohomology.instEpiModuleCatH2π, groupHomology.π_comp_H2Iso_hom_assoc, invariantsAdjunction_homEquiv_symm_apply_hom, hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, trivial_ρ, groupCohomology.toCocycles_comp_isoCocycles₁_hom, MonoidalClosed.linearHomEquiv_symm_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, groupCohomology.mem_cocycles₂_def, groupCohomology.d₂₃_hom_apply, groupHomology.d₁₀_single_one, groupHomology.boundaries₂_le_cycles₂, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupCohomology.d₀₁_comp_d₁₂, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, ihom_obj_V, resCoindToHom_hom_apply_coe, groupCohomology.cocyclesIso₀_hom_comp_f, groupHomology.d₃₂_single, coindToInd_of_support_subset_orbit, groupCohomology.eq_d₀₁_comp_inv, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, groupCohomology.π_comp_H0Iso_hom, groupHomology.H0IsoOfIsTrivial_inv_eq_π, groupCohomology.π_comp_H1Iso_hom_assoc, hom_whiskerRight, groupCohomology.eq_d₁₂_comp_inv, indToCoindAux_self, groupCohomology.mapCocycles₂_comp_i, of_V, groupHomology.eq_d₃₂_comp_inv, invariantsFunctor_obj_carrier, groupCohomology.H0IsoOfIsTrivial_hom, groupCohomology.coe_mapCocycles₁, groupHomology.mem_cycles₂_iff, coindToInd_indToCoind, groupHomology.cyclesMap_comp_isoCycles₂_hom, groupCohomology.d₁₂_hom_apply, groupHomology.comp_d₂₁_eq, groupCohomology.coboundariesToCocycles₁_apply, groupHomology.mapCycles₁_comp_assoc, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, add_hom, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupHomology.H0π_comp_map, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, groupCohomology.comp_d₁₂_eq, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupHomology.δ₀_apply, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, groupHomology.d₃₂_single_one_thd, preservesLimits_forget, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.d₁₂_comp_d₂₃_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, groupCohomology.eq_d₂₃_comp_inv_assoc, finsuppToCoinvariantsTensorFree_single, groupCohomology.eq_d₂₃_comp_inv_apply, hom_surjective, groupCohomology.eq_d₁₂_comp_inv_apply, groupHomology.chains₁ToCoinvariantsKer_surjective, standardComplex.d_eq, groupHomology.cycles₁_eq_top_of_isTrivial, hom_bijective, groupHomology.π_comp_H0Iso_hom_assoc, groupHomology.d₃₂_comp_d₂₁_assoc, groupCohomology.mem_cocycles₁_def, μ_def, hom_id, groupCohomology.mapShortComplexH2_comp_assoc, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, norm_comm_apply, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, groupHomology.d₂₁_single_inv_mul_ρ_add_single, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.cocycles₂_map_one_fst, groupCohomology.mapCocycles₂_comp_i_assoc, groupHomology.d₁₀_comp_coinvariantsMk_apply, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.eq_d₂₁_comp_inv, hom_hom_leftUnitor, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, ihom_ev_app_hom, groupCohomology.dArrowIso₀₁_hom_right, MonoidalClosed.linearHomEquivComm_hom, groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupHomology.mapCycles₁_comp_i, groupCohomology.shortComplexH0_f, groupCohomology.cocyclesOfIsCocycle₁_coe, ActionToRep_obj_V, Representation.equivOfIso_toFun, groupCohomology.coboundaries₂_le_cocycles₂, standardComplex.εToSingle₀_comp_eq, coindVEquiv_symm_apply_coe, liftHomOfSurj_toLinearMap, instEpiModuleCatAppCoinvariantsMk, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, groupCohomology.comp_d₂₃_eq, groupCohomology.coboundaries₂.val_eq_coe, forget_map, ofModuleMonoidAlgebra_obj_coe, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, groupCohomology.d₁₂_apply_mem_cocycles₂, invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, groupCohomology.d₀₁_apply_mem_cocycles₁, groupHomology.cyclesMap_comp_assoc, tensorHomEquiv_apply, indToCoindAux_fst_mul_inv, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, coinvariantsFunctor_obj_carrier, applyAsHom_comm_apply, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupHomology.chainsMap_f_single, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, groupCohomology.subtype_comp_d₀₁_apply, groupCohomology.H2π_eq_iff, groupCohomology.comp_d₀₁_eq, coindFunctorIso_inv_app_hom_toFun_coe, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.cocycles₂_map_one_snd, groupCohomology.δ₁_apply, coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, groupHomology.toCycles_comp_isoCycles₁_hom_apply, δ_def, groupHomology.mapCycles₂_comp_i, groupCohomology.map_H0Iso_hom_f, groupHomology.boundariesOfIsBoundary₁_coe, indToCoindAux_comm, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, res_map_hom_toLinearMap, groupHomology.cyclesIso₀_comp_H0π_apply, groupHomology.eq_d₃₂_comp_inv_apply, forget_obj, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, toAdditive_symm_apply, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, groupCohomology.cocycles₂.coe_mk, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, ofMulDistribMulAction_ρ_apply_apply, RepToAction_map_hom, groupCohomology.instEpiModuleCatH1π, groupCohomology.H2π_comp_map, groupCohomology.cochainsMap_comp_assoc, groupHomology.π_comp_H2Iso_hom, ofHom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, groupCohomology.isoCocycles₂_hom_comp_i, groupCohomology.π_comp_H0Iso_hom_apply, subtype_hom_toFun, groupHomology.coe_mapCycles₂, coinvariantsFunctor_hom_ext_iff, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, groupHomology.H1π_comp_map_apply, groupHomology.H0π_comp_map_assoc, groupCohomology.dArrowIso₀₁_hom_left, trivial_ρ_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.eq_d₀₁_comp_inv_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, groupCohomology.mapCocycles₁_one, groupHomology.H2π_comp_map_assoc, indToCoindAux_mul_fst, groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply, ihom_obj_ρ_apply, smul_hom, mkIso_hom_hom_apply, groupHomology.d₁₀ArrowIso_inv_right, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, hom_braiding, groupCohomology.mem_cocycles₂_iff, tensor_ρ, toAdditive_apply, groupCohomology.H2π_comp_map_assoc, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.d₂₁_comp_d₁₀_apply, hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, hom_injective, ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, groupHomology.H2π_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, zsmul_hom, groupCohomology.inhomogeneousCochains.d_comp_d, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, groupHomology.isoCycles₂_hom_comp_i_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, coinvariantsShortComplex_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, groupHomology.π_comp_H0IsoOfIsTrivial_hom, inv_hom_apply, groupHomology.eq_d₂₁_comp_inv_assoc, nsmul_hom, mkIso_inv_hom_apply, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, coindVEquiv_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, groupHomology.inhomogeneousChains.d_single, groupCohomology.coboundariesOfIsCoboundary₁_coe, groupHomology.cyclesIso₀_inv_comp_iCycles, Representation.coind'_apply_apply, groupCohomology.d₁₂_comp_d₂₃_assoc, groupCohomology.coboundaries₂.coe_mk, RepToAction_obj_V_carrier, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, groupHomology.mapCycles₁_id_comp, trivialFunctor_obj_V, indToCoindAux_mul_snd, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, zero_hom, preservesColimits_forget, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupHomology.eq_d₁₀_comp_inv, hom_inv_rightUnitor, groupHomology.isoShortComplexH1_inv, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, groupHomology.eq_d₁₀_comp_inv_assoc, groupCohomology.d₁₂_comp_d₂₃, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, hom_hom_rightUnitor, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, coe_res_obj_ρ', groupCohomology.H1π_eq_zero_iff, groupHomology.H1AddEquivOfIsTrivial_symm_apply, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, groupCohomology.coboundaries₁.val_eq_coe, groupHomology.d₃₂_single_one_fst, inhomogeneousCochains.d_hom_apply, ρ_mul, coind'_ext_iff, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, groupHomology.d₂₁_comp_d₁₀, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, Representation.equivOfIso_invFun, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, groupHomology.H1ToTensorOfIsTrivial_H1π_single, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, groupCohomology.cocyclesMk₁_eq, sub_hom, groupHomology.cyclesOfIsCycle₁_coe, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, instEpiModuleCatToModuleCatHom, mkIso_inv_hom_toLinearMap, groupHomology.inhomogeneousChains.ext_iff, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, groupHomology.d₂₁_apply_mem_cycles₁, groupCohomology.coboundariesToCocycles₂_apply, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, groupCohomology.H2π_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i_assoc, standardComplex.quasiIso_forget₂_εToSingle₀, groupCohomology.cocycles₁.val_eq_coe, groupCohomology.H1π_comp_map_apply, leftRegularHom_hom_single, groupCohomology.cocycles₁_map_one, homEquiv_apply, groupHomology.eq_d₃₂_comp_inv_assoc, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, coinvariantsAdjunction_unit_app, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, groupHomology.mem_cycles₁_of_mem_boundaries₁, coinvariantsMk_app_hom, forget₂_moduleCat_obj, groupCohomology.cocyclesMap_comp_assoc, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, indCoindIso_hom_hom_toLinearMap, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, groupHomology.H1π_eq_zero_iff, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂, groupHomology.d₂₁_single_one_fst, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.H2π_comp_map, groupHomology.mem_cycles₂_of_mem_boundaries₂, groupCohomology.cocycles₂.val_eq_coe, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, RepToAction_obj_ρ, groupCohomology.eq_d₂₃_comp_inv, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.H1π_comp_map_assoc, groupHomology.instEpiModuleCatH1π, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.H1AddEquivOfIsTrivial_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles, coinvariantsTensor_hom_ext_iff, indResHomEquiv_apply, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.δ₀_apply, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, unit_iso_comm, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, groupHomology.instEpiModuleCatH2π, groupCohomology.cocyclesMk₂_eq, indCoindIso_inv_hom_toLinearMap, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, forget₂_moduleCat_map, groupHomology.d₃₂_apply_mem_cycles₂, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.boundariesOfIsBoundary₂_coe, groupHomology.cyclesMk₁_eq, groupHomology.cyclesIso₀_comp_H0π_assoc, norm_apply, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, groupHomology.instEpiModuleCatH0π, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, linearization_obj_V, groupCohomology.mapCocycles₁_comp_i_apply, groupHomology.mapCycles₂_id_comp_apply, groupCohomology.cocycles₂_ext_iff, MonoidalClosed.linearHomEquiv_hom, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, invariantsAdjunction_homEquiv_apply_hom, hom_comm_apply, groupHomology.H2π_comp_map_apply, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, sum_hom, hom_inv_leftUnitor, groupCohomology.cochainsMap_f_hom, groupCohomology.coboundaries₁_ext_iff, standardComplex.d_apply, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.inhomogeneousChains.d_comp_d, groupHomology.π_comp_H0Iso_hom, hom_inv_associator, quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.π_comp_H2Iso_hom_apply, homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, coinvariantsTensorMk_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap, groupHomology.H0π_comp_H0Iso_hom, groupHomology.isoCycles₁_hom_comp_i_assoc, ihom_map, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, invariantsFunctor_map_hom, id_apply, groupHomology.d₁₀_eq_zero_of_isTrivial, groupCohomology.π_comp_H1Iso_hom_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.d₀₁_comp_d₁₂_assoc, invariantsAdjunction_counit_app, groupHomology.d₂₁_single_one_snd, groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupHomology.d₃₂_comp_d₂₁, groupHomology.d₃₂_single_one_snd, groupHomology.π_comp_H2Iso_hom_apply, coinvariantsTensorIndHom_mk_tmul_indVMk, ihom_coev_app_hom, groupHomology.mapCycles₁_hom, indToCoind_coindToInd, tensorUnit_V, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, groupHomology.single_mem_cycles₁_of_mem_invariants, groupHomology.isoShortComplexH2_inv, groupHomology.coe_mapCycles₁, groupHomology.toCycles_comp_isoCycles₁_hom, groupCohomology.d₀₁_comp_d₁₂_apply, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, Representation.linHom.mem_invariants_iff_comm, comp_apply, hom_tensorHom, indResHomEquiv_symm_apply, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupHomology.boundariesToCycles₂_apply, groupCohomology.subtype_comp_d₀₁, hom_comp, groupHomology.cyclesOfIsCycle₂_coe, groupHomology.isoCycles₂_hom_comp_i, groupHomology.π_comp_H1Iso_hom, groupHomology.isoCycles₂_inv_comp_iCycles, groupHomology.d₁₀_single_inv, groupHomology.mkH1OfIsTrivial_apply, indToCoindAux_snd_mul_inv, instMonoModuleCatToModuleCatHom, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, res_obj_ρ, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, hom_whiskerLeft, groupCohomology.coboundaries₁_le_cocycles₁, groupHomology.shortComplexH0_g, RepToAction_obj, groupHomology.d₁₀ArrowIso_hom_right, groupHomology.single_one_mem_boundaries₁, applyAsHom_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, mkQ_hom_toFun, groupHomology.cyclesIso₀_comp_H0π, groupCohomology.isoCocycles₂_hom_comp_i_apply, groupHomology.d₂₁_single, groupHomology.inhomogeneousChains.d_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, groupHomology.eq_d₂₁_comp_inv_apply, epi_iff_surjective, groupCohomology.coboundaries₂_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MonoidalClosed.linearHomEquivComm_symm_hom, indToCoindAux_of_not_rel, groupCohomology.cocyclesOfIsCocycle₂_coe, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.H0π_comp_H0Iso_hom_assoc, groupCohomology.H1π_comp_map, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, tensor_V, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupCohomology.cocyclesMk₀_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, groupHomology.lsingle_comp_chainsMap_f_assoc, tensorHomEquiv_symm_apply, hom_inv_apply, groupHomology.single_mem_cycles₂_iff, groupCohomology.isoShortComplexH1_inv, groupHomology.boundaries₁_le_cycles₁, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, coinvariantsAdjunction_homEquiv_apply_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, ihom_obj_ρ, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, groupCohomology.cocycles₁_ext_iff, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, groupCohomology.cocycles₁.coe_mk, groupCohomology.eq_d₁₂_comp_inv_assoc, groupCohomology.H1InfRes_f, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, ofHom_apply, groupHomology.d₁₀ArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, groupHomology.single_mem_cycles₁_iff, coinvariantsFunctor_map_hom, groupHomology.d₂₁_single_ρ_add_single_inv_mul, finsupp_V, groupCohomology.isoShortComplexH2_inv, groupCohomology.map_id_comp_H0Iso_hom_assoc, groupCohomology.isoCocycles₂_hom_comp_i_assoc, groupHomology.eq_d₁₀_comp_inv_apply, reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, barComplex.d_single, mono_iff_injective, groupHomology.d₂₁_comp_d₁₀_assoc, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, mkIso_hom_hom_toLinearMap, groupCohomology.isoCocycles₁_hom_comp_i_assoc, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.mapCycles₁_comp_i_assoc, groupHomology.H0π_comp_map_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single, groupCohomology.coboundariesOfIsCoboundary₂_coe, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, groupCohomology.coboundaries₁.coe_mk, groupHomology.mem_cycles₁_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, res_obj_V, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, trivial_V, groupCohomology.cocycles₁.d₁₂_apply, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, groupCohomology.π_comp_H2Iso_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.H2π_eq_zero_iff, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, instIsTrivialVOfCompLinearMapIdρ, groupHomology.δ₁_apply, neg_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1π_eq_iff, groupHomology.d₃₂_comp_d₂₁_apply, groupHomology.chainsMap_f, quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, groupHomology.cyclesMap_comp_isoCycles₁_hom, groupCohomology.d₀₁_eq_zero, coindFunctorIso_hom_app_hom_toFun_hom_toFun
applyAsHom 📖	CompOp	17 math math: FiniteCyclicGroup.chainComplexFunctor_obj, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, FiniteCyclicGroup.groupHomologyπEven_eq_iff, applyAsHom_comm_assoc, FiniteCyclicGroup.chainComplexFunctor_map_f, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, applyAsHom_comm, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, applyAsHom_apply, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff
diagonal 📖	CompOp	2 math math: diagonal_succ_projective, barComplex.d_comp_diagonalSuccIsoFree_inv_eq
diagonalOneIsoLeftRegular 📖	CompOp	—
finsupp 📖	CompOp	1 math math: finsupp_V
finsuppTensorLeft 📖	CompOp	—
finsuppTensorRight 📖	CompOp	—
forgetNatIsoActionForget 📖	CompOp	—
free 📖	CompOp	6 math math: free_projective, coinvariantsTensorFreeLEquiv_apply, inhomogeneousCochains.d_eq, groupHomology.inhomogeneousChains.d_eq, barComplex.d_comp_diagonalSuccIsoFree_inv_eq, barComplex.d_single
freeLift 📖	CompOp	—
freeLiftLEquiv 📖	CompOp	1 math math: inhomogeneousCochains.d_eq
hV1 📖	CompOp	565 math math: groupCohomology.instEpiModuleCatH2π, groupHomology.π_comp_H2Iso_hom_assoc, invariantsAdjunction_homEquiv_symm_apply_hom, hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, trivial_ρ, groupCohomology.toCocycles_comp_isoCocycles₁_hom, MonoidalClosed.linearHomEquiv_symm_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, groupCohomology.mem_cocycles₂_def, groupCohomology.d₂₃_hom_apply, groupHomology.d₁₀_single_one, groupHomology.boundaries₂_le_cycles₂, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupCohomology.d₀₁_comp_d₁₂, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, ihom_obj_V, resCoindToHom_hom_apply_coe, groupCohomology.cocyclesIso₀_hom_comp_f, groupHomology.d₃₂_single, coindToInd_of_support_subset_orbit, groupCohomology.eq_d₀₁_comp_inv, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, groupCohomology.π_comp_H0Iso_hom, groupHomology.H0IsoOfIsTrivial_inv_eq_π, groupCohomology.π_comp_H1Iso_hom_assoc, hom_whiskerRight, groupCohomology.eq_d₁₂_comp_inv, indToCoindAux_self, groupCohomology.mapCocycles₂_comp_i, groupHomology.eq_d₃₂_comp_inv, groupCohomology.H0IsoOfIsTrivial_hom, groupCohomology.coe_mapCocycles₁, groupHomology.mem_cycles₂_iff, coindToInd_indToCoind, groupHomology.cyclesMap_comp_isoCycles₂_hom, groupCohomology.d₁₂_hom_apply, groupHomology.comp_d₂₁_eq, groupCohomology.coboundariesToCocycles₁_apply, groupHomology.mapCycles₁_comp_assoc, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, add_hom, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupHomology.H0π_comp_map, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, groupCohomology.comp_d₁₂_eq, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupHomology.δ₀_apply, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, groupHomology.d₃₂_single_one_thd, preservesLimits_forget, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.d₁₂_comp_d₂₃_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, groupCohomology.eq_d₂₃_comp_inv_assoc, finsuppToCoinvariantsTensorFree_single, groupCohomology.eq_d₂₃_comp_inv_apply, hom_surjective, groupCohomology.eq_d₁₂_comp_inv_apply, groupHomology.chains₁ToCoinvariantsKer_surjective, standardComplex.d_eq, groupHomology.cycles₁_eq_top_of_isTrivial, hom_bijective, groupHomology.π_comp_H0Iso_hom_assoc, groupHomology.d₃₂_comp_d₂₁_assoc, groupCohomology.mem_cocycles₁_def, μ_def, hom_id, groupCohomology.mapShortComplexH2_comp_assoc, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, norm_comm_apply, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, groupHomology.d₂₁_single_inv_mul_ρ_add_single, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.cocycles₂_map_one_fst, groupCohomology.mapCocycles₂_comp_i_assoc, groupHomology.d₁₀_comp_coinvariantsMk_apply, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.eq_d₂₁_comp_inv, hom_hom_leftUnitor, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, ihom_ev_app_hom, groupCohomology.dArrowIso₀₁_hom_right, MonoidalClosed.linearHomEquivComm_hom, groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupHomology.mapCycles₁_comp_i, groupCohomology.shortComplexH0_f, groupCohomology.cocyclesOfIsCocycle₁_coe, Representation.equivOfIso_toFun, groupCohomology.coboundaries₂_le_cocycles₂, standardComplex.εToSingle₀_comp_eq, coindVEquiv_symm_apply_coe, liftHomOfSurj_toLinearMap, instEpiModuleCatAppCoinvariantsMk, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, groupCohomology.comp_d₂₃_eq, groupCohomology.coboundaries₂.val_eq_coe, forget_map, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, groupCohomology.d₁₂_apply_mem_cocycles₂, invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, groupCohomology.d₀₁_apply_mem_cocycles₁, groupHomology.cyclesMap_comp_assoc, tensorHomEquiv_apply, indToCoindAux_fst_mul_inv, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, coinvariantsFunctor_obj_carrier, applyAsHom_comm_apply, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupHomology.chainsMap_f_single, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, groupCohomology.subtype_comp_d₀₁_apply, groupCohomology.H2π_eq_iff, groupCohomology.comp_d₀₁_eq, coindFunctorIso_inv_app_hom_toFun_coe, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.cocycles₂_map_one_snd, groupCohomology.δ₁_apply, coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, groupHomology.toCycles_comp_isoCycles₁_hom_apply, δ_def, groupHomology.mapCycles₂_comp_i, groupCohomology.map_H0Iso_hom_f, groupHomology.boundariesOfIsBoundary₁_coe, indToCoindAux_comm, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, res_map_hom_toLinearMap, groupHomology.cyclesIso₀_comp_H0π_apply, groupHomology.eq_d₃₂_comp_inv_apply, forget_obj, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, toAdditive_symm_apply, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, groupCohomology.cocycles₂.coe_mk, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, ofMulDistribMulAction_ρ_apply_apply, RepToAction_map_hom, groupCohomology.instEpiModuleCatH1π, groupCohomology.H2π_comp_map, groupCohomology.cochainsMap_comp_assoc, groupHomology.π_comp_H2Iso_hom, ofHom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, groupCohomology.isoCocycles₂_hom_comp_i, groupCohomology.π_comp_H0Iso_hom_apply, subtype_hom_toFun, groupHomology.coe_mapCycles₂, coinvariantsFunctor_hom_ext_iff, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, groupHomology.H1π_comp_map_apply, groupHomology.H0π_comp_map_assoc, groupCohomology.dArrowIso₀₁_hom_left, trivial_ρ_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.eq_d₀₁_comp_inv_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, groupCohomology.mapCocycles₁_one, groupHomology.H2π_comp_map_assoc, indToCoindAux_mul_fst, groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply, ihom_obj_ρ_apply, RepToAction_obj_V_isAddCommGroup, smul_hom, mkIso_hom_hom_apply, groupHomology.d₁₀ArrowIso_inv_right, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, hom_braiding, groupCohomology.mem_cocycles₂_iff, tensor_ρ, toAdditive_apply, groupCohomology.H2π_comp_map_assoc, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.d₂₁_comp_d₁₀_apply, hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, hom_injective, ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, groupHomology.H2π_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, zsmul_hom, groupCohomology.inhomogeneousCochains.d_comp_d, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, groupHomology.isoCycles₂_hom_comp_i_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, coinvariantsShortComplex_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, groupHomology.π_comp_H0IsoOfIsTrivial_hom, inv_hom_apply, groupHomology.eq_d₂₁_comp_inv_assoc, nsmul_hom, mkIso_inv_hom_apply, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, coindVEquiv_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, groupHomology.inhomogeneousChains.d_single, groupCohomology.coboundariesOfIsCoboundary₁_coe, groupHomology.cyclesIso₀_inv_comp_iCycles, Representation.coind'_apply_apply, groupCohomology.d₁₂_comp_d₂₃_assoc, groupCohomology.coboundaries₂.coe_mk, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, groupHomology.mapCycles₁_id_comp, indToCoindAux_mul_snd, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, zero_hom, preservesColimits_forget, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupHomology.eq_d₁₀_comp_inv, hom_inv_rightUnitor, groupHomology.isoShortComplexH1_inv, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, groupHomology.eq_d₁₀_comp_inv_assoc, groupCohomology.d₁₂_comp_d₂₃, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, hom_hom_rightUnitor, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, coe_res_obj_ρ', groupCohomology.H1π_eq_zero_iff, groupHomology.H1AddEquivOfIsTrivial_symm_apply, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, groupCohomology.coboundaries₁.val_eq_coe, groupHomology.d₃₂_single_one_fst, inhomogeneousCochains.d_hom_apply, ρ_mul, coind'_ext_iff, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, groupHomology.d₂₁_comp_d₁₀, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, Representation.equivOfIso_invFun, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, groupHomology.H1ToTensorOfIsTrivial_H1π_single, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, groupCohomology.cocyclesMk₁_eq, sub_hom, groupHomology.cyclesOfIsCycle₁_coe, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, instEpiModuleCatToModuleCatHom, mkIso_inv_hom_toLinearMap, groupHomology.inhomogeneousChains.ext_iff, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, groupHomology.d₂₁_apply_mem_cycles₁, groupCohomology.coboundariesToCocycles₂_apply, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, groupCohomology.H2π_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i_assoc, standardComplex.quasiIso_forget₂_εToSingle₀, groupCohomology.cocycles₁.val_eq_coe, groupCohomology.H1π_comp_map_apply, leftRegularHom_hom_single, groupCohomology.cocycles₁_map_one, homEquiv_apply, groupHomology.eq_d₃₂_comp_inv_assoc, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, coinvariantsAdjunction_unit_app, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, groupHomology.mem_cycles₁_of_mem_boundaries₁, coinvariantsMk_app_hom, forget₂_moduleCat_obj, groupCohomology.cocyclesMap_comp_assoc, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, indCoindIso_hom_hom_toLinearMap, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, groupHomology.H1π_eq_zero_iff, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂, groupHomology.d₂₁_single_one_fst, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.H2π_comp_map, groupHomology.mem_cycles₂_of_mem_boundaries₂, groupCohomology.cocycles₂.val_eq_coe, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, RepToAction_obj_ρ, groupCohomology.eq_d₂₃_comp_inv, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.H1π_comp_map_assoc, groupHomology.instEpiModuleCatH1π, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.H1AddEquivOfIsTrivial_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles, coinvariantsTensor_hom_ext_iff, indResHomEquiv_apply, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.δ₀_apply, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, unit_iso_comm, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, groupHomology.instEpiModuleCatH2π, groupCohomology.cocyclesMk₂_eq, indCoindIso_inv_hom_toLinearMap, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, forget₂_moduleCat_map, groupHomology.d₃₂_apply_mem_cycles₂, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.boundariesOfIsBoundary₂_coe, groupHomology.cyclesMk₁_eq, groupHomology.cyclesIso₀_comp_H0π_assoc, norm_apply, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, groupHomology.instEpiModuleCatH0π, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, groupCohomology.mapCocycles₁_comp_i_apply, groupHomology.mapCycles₂_id_comp_apply, groupCohomology.cocycles₂_ext_iff, MonoidalClosed.linearHomEquiv_hom, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, invariantsAdjunction_homEquiv_apply_hom, hom_comm_apply, groupHomology.H2π_comp_map_apply, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, sum_hom, hom_inv_leftUnitor, groupCohomology.cochainsMap_f_hom, groupCohomology.coboundaries₁_ext_iff, standardComplex.d_apply, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.inhomogeneousChains.d_comp_d, groupHomology.π_comp_H0Iso_hom, hom_inv_associator, quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.π_comp_H2Iso_hom_apply, homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, coinvariantsTensorMk_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap, groupHomology.H0π_comp_H0Iso_hom, groupHomology.isoCycles₁_hom_comp_i_assoc, ihom_map, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, invariantsFunctor_map_hom, id_apply, groupHomology.d₁₀_eq_zero_of_isTrivial, groupCohomology.π_comp_H1Iso_hom_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.d₀₁_comp_d₁₂_assoc, invariantsAdjunction_counit_app, groupHomology.d₂₁_single_one_snd, groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupHomology.d₃₂_comp_d₂₁, groupHomology.d₃₂_single_one_snd, groupHomology.π_comp_H2Iso_hom_apply, coinvariantsTensorIndHom_mk_tmul_indVMk, ihom_coev_app_hom, groupHomology.mapCycles₁_hom, indToCoind_coindToInd, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, groupHomology.single_mem_cycles₁_of_mem_invariants, groupHomology.isoShortComplexH2_inv, groupHomology.coe_mapCycles₁, groupHomology.toCycles_comp_isoCycles₁_hom, groupCohomology.d₀₁_comp_d₁₂_apply, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, Representation.linHom.mem_invariants_iff_comm, comp_apply, hom_tensorHom, indResHomEquiv_symm_apply, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupHomology.boundariesToCycles₂_apply, groupCohomology.subtype_comp_d₀₁, hom_comp, groupHomology.cyclesOfIsCycle₂_coe, groupHomology.isoCycles₂_hom_comp_i, groupHomology.π_comp_H1Iso_hom, groupHomology.isoCycles₂_inv_comp_iCycles, groupHomology.d₁₀_single_inv, groupHomology.mkH1OfIsTrivial_apply, indToCoindAux_snd_mul_inv, instMonoModuleCatToModuleCatHom, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, res_obj_ρ, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, hom_whiskerLeft, groupCohomology.coboundaries₁_le_cocycles₁, groupHomology.shortComplexH0_g, RepToAction_obj, groupHomology.d₁₀ArrowIso_hom_right, groupHomology.single_one_mem_boundaries₁, applyAsHom_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, mkQ_hom_toFun, groupHomology.cyclesIso₀_comp_H0π, groupCohomology.isoCocycles₂_hom_comp_i_apply, groupHomology.d₂₁_single, groupHomology.inhomogeneousChains.d_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, groupHomology.eq_d₂₁_comp_inv_apply, epi_iff_surjective, groupCohomology.coboundaries₂_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MonoidalClosed.linearHomEquivComm_symm_hom, indToCoindAux_of_not_rel, groupCohomology.cocyclesOfIsCocycle₂_coe, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.H0π_comp_H0Iso_hom_assoc, groupCohomology.H1π_comp_map, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, tensor_V, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupCohomology.cocyclesMk₀_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, groupHomology.lsingle_comp_chainsMap_f_assoc, tensorHomEquiv_symm_apply, hom_inv_apply, groupHomology.single_mem_cycles₂_iff, groupCohomology.isoShortComplexH1_inv, groupHomology.boundaries₁_le_cycles₁, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, coinvariantsAdjunction_homEquiv_apply_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, ihom_obj_ρ, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, groupCohomology.cocycles₁_ext_iff, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, groupCohomology.cocycles₁.coe_mk, groupCohomology.eq_d₁₂_comp_inv_assoc, groupCohomology.H1InfRes_f, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, ofHom_apply, groupHomology.d₁₀ArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, groupHomology.single_mem_cycles₁_iff, coinvariantsFunctor_map_hom, groupHomology.d₂₁_single_ρ_add_single_inv_mul, finsupp_V, groupCohomology.isoShortComplexH2_inv, groupCohomology.map_id_comp_H0Iso_hom_assoc, groupCohomology.isoCocycles₂_hom_comp_i_assoc, groupHomology.eq_d₁₀_comp_inv_apply, reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, barComplex.d_single, mono_iff_injective, groupHomology.d₂₁_comp_d₁₀_assoc, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, mkIso_hom_hom_toLinearMap, groupCohomology.isoCocycles₁_hom_comp_i_assoc, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.mapCycles₁_comp_i_assoc, groupHomology.H0π_comp_map_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single, groupCohomology.coboundariesOfIsCoboundary₂_coe, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, groupCohomology.coboundaries₁.coe_mk, groupHomology.mem_cycles₁_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, groupCohomology.cocycles₁.d₁₂_apply, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, groupCohomology.π_comp_H2Iso_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.H2π_eq_zero_iff, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, instIsTrivialVOfCompLinearMapIdρ, groupHomology.δ₁_apply, neg_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1π_eq_iff, groupHomology.d₃₂_comp_d₂₁_apply, groupHomology.chainsMap_f, quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, groupHomology.cyclesMap_comp_isoCycles₁_hom, groupCohomology.d₀₁_eq_zero, coindFunctorIso_hom_app_hom_toFun_hom_toFun
hV2 📖	CompOp	560 math math: groupCohomology.instEpiModuleCatH2π, groupHomology.π_comp_H2Iso_hom_assoc, invariantsAdjunction_homEquiv_symm_apply_hom, hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, trivial_ρ, groupCohomology.toCocycles_comp_isoCocycles₁_hom, MonoidalClosed.linearHomEquiv_symm_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, groupCohomology.mem_cocycles₂_def, groupCohomology.d₂₃_hom_apply, groupHomology.d₁₀_single_one, groupHomology.boundaries₂_le_cycles₂, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupCohomology.d₀₁_comp_d₁₂, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, ihom_obj_V, resCoindToHom_hom_apply_coe, groupCohomology.cocyclesIso₀_hom_comp_f, groupHomology.d₃₂_single, coindToInd_of_support_subset_orbit, groupCohomology.eq_d₀₁_comp_inv, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, groupCohomology.π_comp_H0Iso_hom, groupHomology.H0IsoOfIsTrivial_inv_eq_π, groupCohomology.π_comp_H1Iso_hom_assoc, hom_whiskerRight, groupCohomology.eq_d₁₂_comp_inv, indToCoindAux_self, groupCohomology.mapCocycles₂_comp_i, groupHomology.eq_d₃₂_comp_inv, groupCohomology.H0IsoOfIsTrivial_hom, groupCohomology.coe_mapCocycles₁, groupHomology.mem_cycles₂_iff, coindToInd_indToCoind, groupHomology.cyclesMap_comp_isoCycles₂_hom, groupCohomology.d₁₂_hom_apply, groupHomology.comp_d₂₁_eq, groupCohomology.coboundariesToCocycles₁_apply, groupHomology.mapCycles₁_comp_assoc, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, add_hom, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupHomology.H0π_comp_map, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, groupCohomology.comp_d₁₂_eq, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupHomology.δ₀_apply, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, groupHomology.d₃₂_single_one_thd, preservesLimits_forget, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.d₁₂_comp_d₂₃_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, groupCohomology.eq_d₂₃_comp_inv_assoc, finsuppToCoinvariantsTensorFree_single, groupCohomology.eq_d₂₃_comp_inv_apply, hom_surjective, groupCohomology.eq_d₁₂_comp_inv_apply, groupHomology.chains₁ToCoinvariantsKer_surjective, standardComplex.d_eq, groupHomology.cycles₁_eq_top_of_isTrivial, hom_bijective, groupHomology.π_comp_H0Iso_hom_assoc, groupHomology.d₃₂_comp_d₂₁_assoc, groupCohomology.mem_cocycles₁_def, μ_def, hom_id, groupCohomology.mapShortComplexH2_comp_assoc, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, norm_comm_apply, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, groupHomology.d₂₁_single_inv_mul_ρ_add_single, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.cocycles₂_map_one_fst, groupCohomology.mapCocycles₂_comp_i_assoc, groupHomology.d₁₀_comp_coinvariantsMk_apply, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.eq_d₂₁_comp_inv, hom_hom_leftUnitor, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, ihom_ev_app_hom, groupCohomology.dArrowIso₀₁_hom_right, MonoidalClosed.linearHomEquivComm_hom, groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupHomology.mapCycles₁_comp_i, groupCohomology.shortComplexH0_f, groupCohomology.cocyclesOfIsCocycle₁_coe, Representation.equivOfIso_toFun, groupCohomology.coboundaries₂_le_cocycles₂, standardComplex.εToSingle₀_comp_eq, coindVEquiv_symm_apply_coe, liftHomOfSurj_toLinearMap, instEpiModuleCatAppCoinvariantsMk, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, groupCohomology.comp_d₂₃_eq, groupCohomology.coboundaries₂.val_eq_coe, forget_map, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, groupCohomology.d₁₂_apply_mem_cocycles₂, invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, groupCohomology.d₀₁_apply_mem_cocycles₁, groupHomology.cyclesMap_comp_assoc, tensorHomEquiv_apply, indToCoindAux_fst_mul_inv, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, coinvariantsFunctor_obj_carrier, applyAsHom_comm_apply, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupHomology.chainsMap_f_single, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, groupCohomology.subtype_comp_d₀₁_apply, groupCohomology.H2π_eq_iff, groupCohomology.comp_d₀₁_eq, coindFunctorIso_inv_app_hom_toFun_coe, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.cocycles₂_map_one_snd, groupCohomology.δ₁_apply, coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, groupHomology.toCycles_comp_isoCycles₁_hom_apply, δ_def, groupHomology.mapCycles₂_comp_i, groupCohomology.map_H0Iso_hom_f, groupHomology.boundariesOfIsBoundary₁_coe, indToCoindAux_comm, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, res_map_hom_toLinearMap, groupHomology.cyclesIso₀_comp_H0π_apply, groupHomology.eq_d₃₂_comp_inv_apply, forget_obj, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, groupCohomology.cocycles₂.coe_mk, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, ofMulDistribMulAction_ρ_apply_apply, RepToAction_map_hom, groupCohomology.instEpiModuleCatH1π, groupCohomology.H2π_comp_map, groupCohomology.cochainsMap_comp_assoc, groupHomology.π_comp_H2Iso_hom, ofHom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, groupCohomology.isoCocycles₂_hom_comp_i, groupCohomology.π_comp_H0Iso_hom_apply, subtype_hom_toFun, groupHomology.coe_mapCycles₂, coinvariantsFunctor_hom_ext_iff, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, groupHomology.H1π_comp_map_apply, groupHomology.H0π_comp_map_assoc, groupCohomology.dArrowIso₀₁_hom_left, trivial_ρ_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.eq_d₀₁_comp_inv_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, groupCohomology.mapCocycles₁_one, groupHomology.H2π_comp_map_assoc, indToCoindAux_mul_fst, groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply, ihom_obj_ρ_apply, smul_hom, mkIso_hom_hom_apply, groupHomology.d₁₀ArrowIso_inv_right, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, hom_braiding, groupCohomology.mem_cocycles₂_iff, tensor_ρ, groupCohomology.H2π_comp_map_assoc, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.d₂₁_comp_d₁₀_apply, hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, hom_injective, ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, groupHomology.H2π_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, zsmul_hom, groupCohomology.inhomogeneousCochains.d_comp_d, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, groupHomology.isoCycles₂_hom_comp_i_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, coinvariantsShortComplex_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, groupHomology.π_comp_H0IsoOfIsTrivial_hom, inv_hom_apply, groupHomology.eq_d₂₁_comp_inv_assoc, nsmul_hom, mkIso_inv_hom_apply, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, coindVEquiv_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, groupHomology.inhomogeneousChains.d_single, groupCohomology.coboundariesOfIsCoboundary₁_coe, groupHomology.cyclesIso₀_inv_comp_iCycles, Representation.coind'_apply_apply, groupCohomology.d₁₂_comp_d₂₃_assoc, groupCohomology.coboundaries₂.coe_mk, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, RepToAction_obj_V_isModule, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, groupHomology.mapCycles₁_id_comp, indToCoindAux_mul_snd, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, zero_hom, preservesColimits_forget, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupHomology.eq_d₁₀_comp_inv, hom_inv_rightUnitor, groupHomology.isoShortComplexH1_inv, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, groupHomology.eq_d₁₀_comp_inv_assoc, groupCohomology.d₁₂_comp_d₂₃, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, hom_hom_rightUnitor, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, coe_res_obj_ρ', groupCohomology.H1π_eq_zero_iff, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, groupCohomology.coboundaries₁.val_eq_coe, groupHomology.d₃₂_single_one_fst, inhomogeneousCochains.d_hom_apply, ρ_mul, coind'_ext_iff, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, groupHomology.d₂₁_comp_d₁₀, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, Representation.equivOfIso_invFun, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, groupHomology.H1ToTensorOfIsTrivial_H1π_single, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, groupCohomology.cocyclesMk₁_eq, sub_hom, groupHomology.cyclesOfIsCycle₁_coe, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, instEpiModuleCatToModuleCatHom, mkIso_inv_hom_toLinearMap, groupHomology.inhomogeneousChains.ext_iff, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, groupHomology.d₂₁_apply_mem_cycles₁, groupCohomology.coboundariesToCocycles₂_apply, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, groupCohomology.H2π_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i_assoc, standardComplex.quasiIso_forget₂_εToSingle₀, groupCohomology.cocycles₁.val_eq_coe, groupCohomology.H1π_comp_map_apply, leftRegularHom_hom_single, groupCohomology.cocycles₁_map_one, homEquiv_apply, groupHomology.eq_d₃₂_comp_inv_assoc, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, coinvariantsAdjunction_unit_app, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, groupHomology.mem_cycles₁_of_mem_boundaries₁, coinvariantsMk_app_hom, forget₂_moduleCat_obj, groupCohomology.cocyclesMap_comp_assoc, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, indCoindIso_hom_hom_toLinearMap, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, groupHomology.H1π_eq_zero_iff, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂, groupHomology.d₂₁_single_one_fst, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.H2π_comp_map, groupHomology.mem_cycles₂_of_mem_boundaries₂, groupCohomology.cocycles₂.val_eq_coe, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, RepToAction_obj_ρ, groupCohomology.eq_d₂₃_comp_inv, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.H1π_comp_map_assoc, groupHomology.instEpiModuleCatH1π, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.isoCocycles₂_inv_comp_iCocycles, coinvariantsTensor_hom_ext_iff, indResHomEquiv_apply, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.δ₀_apply, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, unit_iso_comm, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, groupHomology.instEpiModuleCatH2π, groupCohomology.cocyclesMk₂_eq, indCoindIso_inv_hom_toLinearMap, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, forget₂_moduleCat_map, groupHomology.d₃₂_apply_mem_cycles₂, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.boundariesOfIsBoundary₂_coe, groupHomology.cyclesMk₁_eq, groupHomology.cyclesIso₀_comp_H0π_assoc, norm_apply, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, groupHomology.instEpiModuleCatH0π, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, groupCohomology.mapCocycles₁_comp_i_apply, groupHomology.mapCycles₂_id_comp_apply, groupCohomology.cocycles₂_ext_iff, MonoidalClosed.linearHomEquiv_hom, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, invariantsAdjunction_homEquiv_apply_hom, hom_comm_apply, groupHomology.H2π_comp_map_apply, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, sum_hom, hom_inv_leftUnitor, groupCohomology.cochainsMap_f_hom, groupCohomology.coboundaries₁_ext_iff, standardComplex.d_apply, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.inhomogeneousChains.d_comp_d, groupHomology.π_comp_H0Iso_hom, hom_inv_associator, quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.π_comp_H2Iso_hom_apply, homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, coinvariantsTensorMk_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap, groupHomology.H0π_comp_H0Iso_hom, groupHomology.isoCycles₁_hom_comp_i_assoc, ihom_map, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, invariantsFunctor_map_hom, id_apply, groupHomology.d₁₀_eq_zero_of_isTrivial, groupCohomology.π_comp_H1Iso_hom_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.d₀₁_comp_d₁₂_assoc, invariantsAdjunction_counit_app, groupHomology.d₂₁_single_one_snd, groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc, groupHomology.d₃₂_comp_d₂₁, groupHomology.d₃₂_single_one_snd, groupHomology.π_comp_H2Iso_hom_apply, coinvariantsTensorIndHom_mk_tmul_indVMk, ihom_coev_app_hom, groupHomology.mapCycles₁_hom, indToCoind_coindToInd, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, groupHomology.single_mem_cycles₁_of_mem_invariants, groupHomology.isoShortComplexH2_inv, groupHomology.coe_mapCycles₁, groupHomology.toCycles_comp_isoCycles₁_hom, groupCohomology.d₀₁_comp_d₁₂_apply, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, Representation.linHom.mem_invariants_iff_comm, comp_apply, hom_tensorHom, indResHomEquiv_symm_apply, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupHomology.boundariesToCycles₂_apply, groupCohomology.subtype_comp_d₀₁, hom_comp, groupHomology.cyclesOfIsCycle₂_coe, groupHomology.isoCycles₂_hom_comp_i, groupHomology.π_comp_H1Iso_hom, groupHomology.isoCycles₂_inv_comp_iCycles, groupHomology.d₁₀_single_inv, groupHomology.mkH1OfIsTrivial_apply, indToCoindAux_snd_mul_inv, instMonoModuleCatToModuleCatHom, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, res_obj_ρ, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, hom_whiskerLeft, groupCohomology.coboundaries₁_le_cocycles₁, groupHomology.shortComplexH0_g, RepToAction_obj, groupHomology.d₁₀ArrowIso_hom_right, groupHomology.single_one_mem_boundaries₁, applyAsHom_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, mkQ_hom_toFun, groupHomology.cyclesIso₀_comp_H0π, groupCohomology.isoCocycles₂_hom_comp_i_apply, groupHomology.d₂₁_single, groupHomology.inhomogeneousChains.d_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, groupHomology.eq_d₂₁_comp_inv_apply, epi_iff_surjective, groupCohomology.coboundaries₂_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MonoidalClosed.linearHomEquivComm_symm_hom, indToCoindAux_of_not_rel, groupCohomology.cocyclesOfIsCocycle₂_coe, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.H0π_comp_H0Iso_hom_assoc, groupCohomology.H1π_comp_map, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, tensor_V, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupCohomology.cocyclesMk₀_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, groupHomology.lsingle_comp_chainsMap_f_assoc, tensorHomEquiv_symm_apply, hom_inv_apply, groupHomology.single_mem_cycles₂_iff, groupCohomology.isoShortComplexH1_inv, groupHomology.boundaries₁_le_cycles₁, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, coinvariantsAdjunction_homEquiv_apply_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, ihom_obj_ρ, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, groupCohomology.cocycles₁_ext_iff, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, groupCohomology.cocycles₁.coe_mk, groupCohomology.eq_d₁₂_comp_inv_assoc, groupCohomology.H1InfRes_f, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, ofHom_apply, groupHomology.d₁₀ArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, groupHomology.single_mem_cycles₁_iff, coinvariantsFunctor_map_hom, groupHomology.d₂₁_single_ρ_add_single_inv_mul, groupCohomology.isoShortComplexH2_inv, groupCohomology.map_id_comp_H0Iso_hom_assoc, groupCohomology.isoCocycles₂_hom_comp_i_assoc, groupHomology.eq_d₁₀_comp_inv_apply, reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, barComplex.d_single, mono_iff_injective, groupHomology.d₂₁_comp_d₁₀_assoc, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, mkIso_hom_hom_toLinearMap, groupCohomology.isoCocycles₁_hom_comp_i_assoc, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.mapCycles₁_comp_i_assoc, groupHomology.H0π_comp_map_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single, groupCohomology.coboundariesOfIsCoboundary₂_coe, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, groupCohomology.coboundaries₁.coe_mk, groupHomology.mem_cycles₁_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, groupCohomology.cocycles₁.d₁₂_apply, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, groupCohomology.π_comp_H2Iso_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.H2π_eq_zero_iff, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, instIsTrivialVOfCompLinearMapIdρ, groupHomology.δ₁_apply, neg_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1π_eq_iff, groupHomology.d₃₂_comp_d₂₁_apply, groupHomology.chainsMap_f, quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, groupHomology.cyclesMap_comp_isoCycles₁_hom, groupCohomology.d₀₁_eq_zero, coindFunctorIso_hom_app_hom_toFun_hom_toFun
hasForgetToModuleCat 📖	CompOp	32 math math: groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, preservesLimits_forget, groupHomology.π_comp_H0Iso_hom_assoc, standardComplex.εToSingle₀_comp_eq, instEpiModuleCatAppCoinvariantsMk, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.coinvariantsMk_comp_H0Iso_inv, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coinvariantsFunctor_hom_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk, preservesColimits_forget, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, standardComplex.quasiIso_forget₂_εToSingle₀, coinvariantsAdjunction_unit_app, coinvariantsMk_app_hom, forget₂_moduleCat_obj, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, forget₂_moduleCat_map, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.π_comp_H0Iso_hom, groupHomology.H0π_comp_H0Iso_hom, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupHomology.shortComplexH0_g, groupHomology.d₁₀_comp_coinvariantsMk_assoc, groupHomology.H0π_comp_H0Iso_hom_assoc, coinvariantsAdjunction_homEquiv_apply_hom, groupHomology.H0π_comp_H0Iso_hom_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc
homEquiv 📖	CompOp	3 math math: homEquiv_apply, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, homEquiv_symm_apply
homLinearEquiv 📖	CompOp	—
ihom 📖	CompOp	7 math math: ihom_obj_V, tensorHomEquiv_apply, ihom_obj_ρ_apply, ihom_map, tensorHomEquiv_symm_apply, ihom_obj_ρ, ihom_obj_ρ_def
instAddCommGroupHom 📖	CompOp	25 math math: MonoidalClosed.linearHomEquiv_symm_hom, MonoidalClosed.linearHomEquivComm_hom, coindVEquiv_symm_apply_coe, coindFunctorIso_inv_app_hom_toFun_coe, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, coindResAdjunction_homEquiv_apply, coindVEquiv_apply, Representation.coind'_apply_apply, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, coindResAdjunction_homEquiv_symm_apply, indResHomEquiv_apply, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, resCoindHomEquiv_apply, MonoidalClosed.linearHomEquiv_hom, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, sum_hom, ofHom_sum, indResHomEquiv_symm_apply, MonoidalClosed.linearHomEquivComm_symm_hom, coindFunctorIso_hom_app_hom_toFun_hom_toFun
instAddHom 📖	CompOp	4 math math: add_hom, ofHom_add, add_comp, comp_add
instBraidedCategory 📖	CompOp	1 math math: hom_braiding
instCategory 📖	CompOp	384 math math: invariantsAdjunction_homEquiv_symm_apply_hom, hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, μ_hom, MonoidalClosed.linearHomEquiv_symm_hom, groupHomology.map₁_quotientGroupMk'_epi, groupHomology.coinfNatTrans_app, groupHomology.mapShortComplexH2_id, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, ofHom_sub, groupCohomology.δ_apply, groupCohomology.cocyclesMap_id_comp_assoc, groupHomology.mono_δ_of_isZero, coindResAdjunction_counit_app, ihom_obj_V, groupHomology.mapCycles₁_comp_apply, groupHomology.mapShortComplexH1_zero, hom_whiskerRight, groupHomology.cyclesMap_id_comp, indFunctor_obj, groupHomology.mapShortComplexH2_zero, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, indCoindNatIso_hom_app, groupHomology.chainsMap_id, invariantsFunctor_obj_carrier, barComplex.d_def, full_res, instAdditiveResFunctor, coindFunctor_map, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, instIsRightAdjointCoindFunctor, groupHomology.mapCycles₁_comp_assoc, add_hom, instIsTrivialObjModuleCatTrivialFunctor, coinvariantsAdjunction_counit_app, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, groupHomology.map_id, groupCohomology.cochainsMap_comp, groupHomology.δ₀_apply, preservesLimits_forget, groupHomology.coresNatTrans_app, instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, of_tensor, ε_def, groupCohomology.congr, standardComplex.d_eq, ofHom_comp, groupHomology.π_comp_H0Iso_hom_assoc, trivial_projective_of_subsingleton, μ_def, hom_id, groupCohomology.mapShortComplexH2_comp_assoc, FiniteCyclicGroup.chainComplexFunctor_obj, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, norm_comm_apply, coinvariantsAdjunction_homEquiv_symm_apply_hom, free_projective, groupHomology.d₁₀_comp_coinvariantsMk_apply, groupHomology.mapCycles₁_id_comp_assoc, hom_hom_leftUnitor, instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra, ActionToRep_obj_ρ, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, instLinearModuleCatObjFunctorCoinvariantsTensor, groupHomology.mapCycles₁_comp, groupHomology.map_comp, ihom_ev_app_hom, MonoidalClosed.linearHomEquivComm_hom, instIsRightAdjointModuleCatInvariantsFunctor, groupCohomology.map_comp, groupHomology.map_id_comp, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, coinvariantsTensorIndIso_inv, groupHomology.functor_obj, ActionToRep_obj_V, Representation.equivOfIso_toFun, standardComplex.εToSingle₀_comp_eq, coindVEquiv_symm_apply_coe, instEpiModuleCatAppCoinvariantsMk, homEquiv_def, ofHom_add, forget_map, instHasFiniteProducts, ofModuleMonoidAlgebra_obj_coe, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, diagonal_succ_projective, groupHomology.cyclesMap_comp_assoc, tensorHomEquiv_apply, coinvariantsFunctor_obj_carrier, applyAsHom_comm_apply, coindFunctorIso_inv_app_hom_toFun_coe, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, instProjective, groupCohomology.δ₁_apply, coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, δ_def, coinvariantsTensorIndIso_hom, barResolution_complex, groupCohomology.cochainsMap_zero, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, coinvariantsTensorIndNatIso_inv_app, res_map_hom_toLinearMap, groupHomology.epi_δ_of_isZero, groupHomology.map_chainsFunctor_shortExact, forget_obj, instAdditiveModuleCatObjFunctorCoinvariantsTensor, coindResAdjunction_unit_app, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.epi_δ_of_isZero, groupCohomology.cochainsMap_id_comp, groupCohomology.map_id, groupCohomology.mapShortComplexH2_comp, RepToAction_map_hom, groupCohomology.cochainsMap_comp_assoc, instIsRightAdjointResFunctor, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, resIndAdjunction_homEquiv_symm_apply, coinvariantsFunctor_hom_ext_iff, instLinearModuleCatCoinvariantsFunctor, normNatTrans_app, groupHomology.π_comp_H0Iso_hom_apply, applyAsHom_comm_assoc, groupHomology.chainsFunctor_obj, instEnoughProjectives, groupCohomology.functor_obj, groupCohomology.cocyclesMap_comp, ihom_obj_ρ_apply, RepToAction_obj_V_isAddCommGroup, instPreservesZeroMorphismsModuleCatInvariantsFunctor, smul_hom, mkIso_hom_hom_apply, FiniteCyclicGroup.chainComplexFunctor_map_f, smul_comp, groupCohomology.resNatTrans_app, hom_braiding, groupCohomology.mapShortComplexH2_zero, tensor_ρ, resIndAdjunction_homEquiv_apply, groupHomology.d₁₀_comp_coinvariantsMk, hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, groupHomology.chainsMap_id_comp, groupCohomology.mapShortComplexH1_id, coinvariantsShortComplex_g, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, zsmul_hom, coindResAdjunction_homEquiv_apply, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, Tor_map, ofModuleMonoidAlgebra_obj_ρ, coinvariantsShortComplex_f, resIndAdjunction_counit_app, inv_hom_apply, nsmul_hom, instLinearResFunctor, mkIso_inv_hom_apply, instIsLeftAdjointModuleCatCoinvariantsFunctor, coindVEquiv_apply, instMonoidalPreadditive, ActionToRep_map, Representation.coind'_apply_apply, groupHomology.map_id_comp_H0Iso_hom_assoc, RepToAction_obj_V_carrier, RepToAction_obj_V_isModule, groupCohomology.mapShortComplexH2_id_comp_assoc, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.mapShortComplexH2_comp, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.mapCycles₁_id_comp, trivialFunctor_obj_V, zero_hom, δ_hom, preservesColimits_forget, ofHom_nsmul, hom_inv_rightUnitor, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, hom_hom_rightUnitor, linearization_obj_ρ, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, groupHomology.chainsMap_comp, instLinearModuleCatInvariantsFunctor, Representation.equivOfIso_invFun, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, groupCohomology.map_id_comp_assoc, sub_hom, ε_hom, isZero_Tor_succ_of_projective, mkIso_inv_hom_toLinearMap, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, coinvariantsTensorIndNatIso_hom_app, groupHomology.congr, standardComplex.quasiIso_forget₂_εToSingle₀, applyAsHom_comm, homEquiv_apply, coinvariantsAdjunction_unit_app, groupCohomology.H1InfRes_g, standardComplex.d_comp_ε, groupHomology.δ_apply, coinvariantsMk_app_hom, indCoindNatIso_inv_app, instIsEquivalenceActionModuleCatRepToAction, forget₂_moduleCat_obj, groupCohomology.mapShortComplexH1_id_comp, groupCohomology.cocyclesMap_comp_assoc, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, coindResAdjunction_homEquiv_symm_apply, indCoindIso_hom_hom_toLinearMap, groupCohomology.mapShortComplexH1_comp, groupHomology.pOpcycles_comp_opcyclesIso_hom, trivialFunctor_map_hom, η_hom, RepToAction_obj_ρ, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.mapShortComplexH1_id, groupCohomology.map_id_comp, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, coinvariantsTensor_hom_ext_iff, indResHomEquiv_apply, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.δ₀_apply, unit_iso_comm, linearization_map, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, FiniteCyclicGroup.resolution_complex, groupHomology.chainsFunctor_map, indCoindIso_inv_hom_toLinearMap, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, forget₂_moduleCat_map, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.map_id_comp_H0Iso_hom_apply, resCoindHomEquiv_apply, groupHomology.H1CoresCoinfOfTrivial_f, coindFunctor'_obj, instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype, groupHomology.functor_map, linearization_obj_V, groupHomology.mapCycles₂_id_comp_apply, mkIso_hom_hom, standardComplex.instQuasiIsoNatεToSingle₀, standardComplex.x_projective, instIsLeftAdjointResFunctor, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, MonoidalClosed.linearHomEquiv_hom, invariantsAdjunction_homEquiv_apply_hom, instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, FiniteCyclicGroup.resolution_quasiIso, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, η_def, sum_hom, groupCohomology.H1Map_id, hom_inv_leftUnitor, indFunctor_map, standardComplex.d_apply, groupHomology.H1CoresCoinfOfTrivial_g, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.π_comp_H0Iso_hom, hom_inv_associator, groupCohomology.mapShortComplexH1_id_comp_assoc, quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.mapShortComplexH1_zero, homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, coinvariantsTensorMk_apply, groupHomology.H0π_comp_H0Iso_hom, add_comp, coinvariantsShortComplex_X₁, ihom_map, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, invariantsFunctor_map_hom, groupHomology.map_id_comp_H0Iso_hom, id_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.cocyclesMap_id, invariantsAdjunction_counit_app, instHasBinaryBiproducts, norm_comm_assoc, groupCohomology.mapShortComplexH2_id_comp, resIndAdjunction_unit_app, coinvariantsTensorIndHom_mk_tmul_indVMk, ihom_coev_app_hom, leftRegular_projective, tensorUnit_V, groupHomology.chainsMap_zero, groupHomology.isIso_δ_of_isZero, groupHomology.mapShortComplexH2_id_comp, comp_smul, ofHom_sum, comp_apply, hom_tensorHom, indResHomEquiv_symm_apply, hom_comp, groupCohomology.map_cochainsFunctor_shortExact, groupCohomology.cocyclesMap_id_comp, hom_whiskerLeft, groupHomology.shortComplexH0_g, RepToAction_obj, groupCohomology.mapShortComplexH2_id, comp_add, instIsEquivalenceActionModuleCatActionToRep, groupHomology.inhomogeneousChains.d_eq, epi_iff_surjective, groupCohomology.cochainsFunctor_map, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MonoidalClosed.linearHomEquivComm_symm_hom, coinvariantsShortComplex_X₂, groupHomology.H0π_comp_H0Iso_hom_assoc, ofHom_zsmul, groupHomology.cyclesMap_comp, ofHom_id, tensor_V, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, tensorHomEquiv_symm_apply, hom_inv_apply, tensorUnit_ρ, instMonoidalLinear, instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, coinvariantsAdjunction_homEquiv_apply_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomology.H1CoresCoinf_f, ihom_obj_ρ, groupCohomology.cochainsMap_id_comp_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, instIsLeftAdjointIndFunctor, instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, groupHomology.cyclesMap_id, instFaithfulResFunctor, instAdditiveModuleCatInvariantsFunctor, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, ofHom_apply, barComplex.d_comp_diagonalSuccIsoFree_inv_eq, coindFunctor'_map, coinvariantsFunctor_map_hom, coindFunctor_obj, groupCohomology.map_id_comp_H0Iso_hom_assoc, ihom_obj_ρ_def, coinvariantsShortComplex_X₃, reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, mono_iff_injective, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.functor_map, mkIso_hom_hom_toLinearMap, Tor_obj, groupCohomology.mono_δ_of_isZero, coinvariantsShortComplex_shortExact, FiniteCyclicGroup.resolution_π, ofHom_zero, groupHomology.mapCycles₁_quotientGroupMk'_epi, instHasZeroObject, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, instAdditiveModuleCatCoinvariantsFunctor, groupCohomology.cochainsFunctor_obj, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, ofHom_smul, ofHom_neg, groupCohomology.isIso_δ_of_isZero, norm_comm, groupHomology.δ₁_apply, neg_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, quotientToCoinvariantsFunctor_obj_V, groupCohomology.map_comp_assoc, groupCohomology.cochainsMap_id, instInjective, coindFunctorIso_hom_app_hom_toFun_hom_toFun
instCoeSortType 📖	CompOp	—
instConcreteCategoryIntertwiningMapVρ 📖	CompOp	47 math math: groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, preservesLimits_forget, groupHomology.π_comp_H0Iso_hom_assoc, norm_comm_apply, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Representation.equivOfIso_toFun, standardComplex.εToSingle₀_comp_eq, instEpiModuleCatAppCoinvariantsMk, forget_map, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, applyAsHom_comm_apply, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.coinvariantsMk_comp_H0Iso_inv, forget_obj, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coinvariantsFunctor_hom_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk, preservesColimits_forget, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, Representation.equivOfIso_invFun, standardComplex.quasiIso_forget₂_εToSingle₀, coinvariantsAdjunction_unit_app, coinvariantsMk_app_hom, forget₂_moduleCat_obj, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, forget₂_moduleCat_map, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.π_comp_H0Iso_hom, groupHomology.H0π_comp_H0Iso_hom, FDRep.forget₂_ρ, id_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, comp_apply, groupHomology.shortComplexH0_g, groupHomology.d₁₀_comp_coinvariantsMk_assoc, groupHomology.H0π_comp_H0Iso_hom_assoc, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, coinvariantsAdjunction_homEquiv_apply_hom, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, ofHom_apply, reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc
instInhabited 📖	CompOp	—
instLinear 📖	CompOp	9 math math: instLinearModuleCatObjFunctorCoinvariantsTensor, instLinearModuleCatCoinvariantsFunctor, instLinearResFunctor, instLinearModuleCatInvariantsFunctor, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, inhomogeneousCochains.d_eq, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, instMonoidalLinear
instModuleHom 📖	CompOp	23 math math: MonoidalClosed.linearHomEquiv_symm_hom, MonoidalClosed.linearHomEquivComm_hom, coindVEquiv_symm_apply_coe, coindFunctorIso_inv_app_hom_toFun_coe, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, coindResAdjunction_homEquiv_apply, coindVEquiv_apply, Representation.coind'_apply_apply, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, coindResAdjunction_homEquiv_symm_apply, indResHomEquiv_apply, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, resCoindHomEquiv_apply, MonoidalClosed.linearHomEquiv_hom, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, indResHomEquiv_symm_apply, MonoidalClosed.linearHomEquivComm_symm_hom, coindFunctorIso_hom_app_hom_toFun_hom_toFun
instMonoidalActionTypeLinearization 📖	CompOp	8 math math: μ_hom, ε_def, μ_def, δ_def, δ_hom, ε_hom, η_hom, η_def
instMonoidalCategory 📖	CompOp	38 math math: hom_hom_associator, μ_hom, MonoidalClosed.linearHomEquiv_symm_hom, hom_whiskerRight, of_tensor, ε_def, μ_def, hom_hom_leftUnitor, ihom_ev_app_hom, MonoidalClosed.linearHomEquivComm_hom, homEquiv_def, tensorHomEquiv_apply, coinvariantsTensorFreeLEquiv_apply, δ_def, hom_braiding, tensor_ρ, instMonoidalPreadditive, δ_hom, hom_inv_rightUnitor, hom_hom_rightUnitor, ε_hom, η_hom, MonoidalClosed.linearHomEquiv_hom, η_def, hom_inv_leftUnitor, hom_inv_associator, coinvariantsTensorMk_apply, ihom_coev_app_hom, tensorUnit_V, hom_tensorHom, hom_whiskerLeft, groupHomology.inhomogeneousChains.d_eq, MonoidalClosed.linearHomEquivComm_symm_hom, tensor_V, tensorHomEquiv_symm_apply, tensorUnit_ρ, instMonoidalLinear, ihom_obj_ρ_def
instMonoidalClosed 📖	CompOp	8 math math: MonoidalClosed.linearHomEquiv_symm_hom, ihom_ev_app_hom, MonoidalClosed.linearHomEquivComm_hom, homEquiv_def, MonoidalClosed.linearHomEquiv_hom, ihom_coev_app_hom, MonoidalClosed.linearHomEquivComm_symm_hom, ihom_obj_ρ_def
instNegHom 📖	CompOp	2 math math: ofHom_neg, neg_hom
instPreadditive 📖	CompOp	64 math math: groupCohomology.δ_apply, groupHomology.mono_δ_of_isZero, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, barComplex.d_def, instAdditiveResFunctor, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, groupHomology.δ₀_apply, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, standardComplex.d_eq, FiniteCyclicGroup.chainComplexFunctor_obj, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, instLinearModuleCatObjFunctorCoinvariantsTensor, standardComplex.εToSingle₀_comp_eq, groupCohomology.δ₁_apply, barResolution_complex, groupHomology.epi_δ_of_isZero, groupHomology.map_chainsFunctor_shortExact, instAdditiveModuleCatObjFunctorCoinvariantsTensor, groupCohomology.epi_δ_of_isZero, instLinearModuleCatCoinvariantsFunctor, instPreservesZeroMorphismsModuleCatInvariantsFunctor, FiniteCyclicGroup.chainComplexFunctor_map_f, coinvariantsShortComplex_g, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, coinvariantsShortComplex_f, instLinearResFunctor, instMonoidalPreadditive, instLinearModuleCatInvariantsFunctor, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, standardComplex.quasiIso_forget₂_εToSingle₀, standardComplex.d_comp_ε, groupHomology.δ_apply, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.δ₀_apply, FiniteCyclicGroup.resolution_complex, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, standardComplex.instQuasiIsoNatεToSingle₀, standardComplex.x_projective, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, FiniteCyclicGroup.resolution_quasiIso, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, standardComplex.d_apply, coinvariantsShortComplex_X₁, instHasBinaryBiproducts, groupHomology.isIso_δ_of_isZero, groupCohomology.map_cochainsFunctor_shortExact, coinvariantsShortComplex_X₂, instMonoidalLinear, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, instAdditiveModuleCatInvariantsFunctor, barComplex.d_comp_diagonalSuccIsoFree_inv_eq, coinvariantsShortComplex_X₃, groupCohomology.mono_δ_of_isZero, coinvariantsShortComplex_shortExact, FiniteCyclicGroup.resolution_π, FiniteCyclicGroup.resolution.π_f, instAdditiveModuleCatCoinvariantsFunctor, groupCohomology.isIso_δ_of_isZero, groupHomology.δ₁_apply, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
instSMulHom 📖	CompOp	4 math math: smul_hom, smul_comp, comp_smul, ofHom_smul
instSMulIntHom 📖	CompOp	2 math math: zsmul_hom, ofHom_zsmul
instSMulNatHom 📖	CompOp	2 math math: nsmul_hom, ofHom_nsmul
instSubHom 📖	CompOp	16 math math: ofHom_sub, FiniteCyclicGroup.chainComplexFunctor_obj, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, FiniteCyclicGroup.groupHomologyπEven_eq_iff, FiniteCyclicGroup.chainComplexFunctor_map_f, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, sub_hom, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff
instSymmetricCategory 📖	CompOp	—
instZeroHom 📖	CompOp	9 math math: groupHomology.mapShortComplexH1_zero, groupHomology.mapShortComplexH2_zero, groupCohomology.cochainsMap_zero, groupCohomology.mapShortComplexH2_zero, zero_hom, standardComplex.d_comp_ε, groupCohomology.mapShortComplexH1_zero, groupHomology.chainsMap_zero, ofHom_zero
leftRegular 📖	CompOp	17 math math: coindVEquiv_symm_apply_coe, coindFunctorIso_inv_app_hom_toFun_coe, coindVEquiv_apply, Representation.coind'_apply_apply, coind'_ext_iff, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, leftRegularHom_hom_single, leftRegularHomEquiv_symm_single, FiniteCyclicGroup.resolution_complex, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, FiniteCyclicGroup.resolution_quasiIso, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, leftRegular_projective, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, coindFunctorIso_hom_app_hom_toFun_hom_toFun
leftRegularHom 📖	CompOp	2 math math: leftRegularHom_hom_single, FiniteCyclicGroup.resolution.π_f
leftRegularHomEquiv 📖	CompOp	2 math math: Representation.coind'_apply_apply, leftRegularHomEquiv_symm_single
leftRegularTensorTrivialIsoFree 📖	CompOp	—
linearization 📖	CompOp	11 math math: μ_hom, ε_def, μ_def, δ_def, δ_hom, linearization_obj_ρ, ε_hom, η_hom, linearization_map, linearization_obj_V, η_def
linearizationOfMulActionIso 📖	CompOp	—
linearizationTrivialIso 📖	CompOp	—
mkIso 📖	CompOp	5 math math: mkIso_hom_hom_apply, mkIso_inv_hom_apply, mkIso_inv_hom_toLinearMap, mkIso_hom_hom, mkIso_hom_hom_toLinearMap
mkQ 📖	CompOp	1 math math: mkQ_hom_toFun
norm 📖	CompOp	14 math math: FiniteCyclicGroup.chainComplexFunctor_obj, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, normNatTrans_app, FiniteCyclicGroup.chainComplexFunctor_map_f, groupCohomology.norm_ofAlgebraAutOnUnits_eq, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, norm_apply, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, norm_comm_assoc, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, norm_comm
normNatTrans 📖	CompOp	1 math math: normNatTrans_app
of 📖	CompOp	34 math math: ofHom_sub, of_V, hom_ofHom, of_tensor, ofHom_comp, groupCohomology.mapShortComplexH2_comp_assoc, ofHom_add, groupCohomology.infNatTrans_app, groupCohomology.cochainsMap_comp_assoc, mkIso_hom_hom_apply, mkIso_inv_hom_apply, ofHom_nsmul, of_ρ, mkIso_inv_hom_toLinearMap, groupCohomology.cocyclesMap_comp_assoc, indCoindIso_hom_hom_toLinearMap, trivialFunctor_map_hom, indCoindIso_inv_hom_toLinearMap, mkIso_hom_hom, quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.mapShortComplexH1_comp_assoc, ofHom_sum, instIsTrivialOfOfIsTrivial, ofHom_zsmul, ofHom_id, groupCohomology.H1InfRes_f, ofHom_apply, mkIso_hom_hom_toLinearMap, ofHom_zero, ofHom_smul, ofHom_neg, instIsTrivialVOfCompLinearMapIdρ, groupCohomology.map_comp_assoc, coindFunctorIso_hom_app_hom_toFun_hom_toFun
ofAlgebraAut 📖	CompOp	—
ofAlgebraAutOnUnits 📖	CompOp	1 math math: groupCohomology.norm_ofAlgebraAutOnUnits_eq
ofDistribMulAction 📖	CompOp	9 math math: groupCohomology.cocyclesOfIsCocycle₁_coe, groupHomology.boundariesOfIsBoundary₁_coe, ofDistribMulAction_ρ_apply_apply, groupCohomology.coboundariesOfIsCoboundary₁_coe, groupHomology.cyclesOfIsCycle₁_coe, groupHomology.boundariesOfIsBoundary₂_coe, groupHomology.cyclesOfIsCycle₂_coe, groupCohomology.cocyclesOfIsCocycle₂_coe, groupCohomology.coboundariesOfIsCoboundary₂_coe
ofHom 📖	CompOp	45 math math: groupHomology.mapCycles₂_comp_assoc, ofHom_sub, groupHomology.mapCycles₁_comp_apply, hom_ofHom, groupHomology.mapCycles₁_comp_assoc, ε_def, ofHom_comp, μ_def, groupCohomology.mapShortComplexH2_comp_assoc, ofHom_add, groupCohomology.infNatTrans_app, groupHomology.cyclesMap_comp_assoc, tensorHomEquiv_apply, δ_def, groupHomology.map_comp_assoc, groupCohomology.cochainsMap_comp_assoc, ofHom_hom, groupHomology.mapCycles₂_comp_apply, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, coinvariantsShortComplex_f, coindVEquiv_apply, ActionToRep_map, ofHom_nsmul, coinvariantsAdjunction_unit_app, groupCohomology.cocyclesMap_comp_assoc, indResHomEquiv_apply, linearization_map, η_def, quotientToCoinvariantsFunctor_map_hom_toLinearMap, homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, ihom_map, invariantsAdjunction_counit_app, ofHom_sum, indResHomEquiv_symm_apply, ofHom_zsmul, ofHom_id, tensorHomEquiv_symm_apply, groupCohomology.H1InfRes_f, ofHom_apply, ofHom_zero, ofHom_smul, ofHom_neg, groupCohomology.map_comp_assoc
ofMulAction 📖	CompOp	1 math math: standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq
ofMulActionSubsingletonIsoTrivial 📖	CompOp	—
ofMulDistribMulAction 📖	CompOp	7 math math: toAdditive_symm_apply, ofMulDistribMulAction_ρ_apply_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, toAdditive_apply, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, groupCohomology.cocyclesOfIsMulCocycle₁_coe
quotient 📖	CompOp	1 math math: mkQ_hom_toFun
repIsoAction 📖	CompOp	—
subrepresentation 📖	CompOp	1 math math: subtype_hom_toFun
subtype 📖	CompOp	1 math math: subtype_hom_toFun
tensorHomEquiv 📖	CompOp	3 math math: homEquiv_def, tensorHomEquiv_apply, tensorHomEquiv_symm_apply
trivial 📖	CompOp	20 math math: trivial_ρ, coinvariantsAdjunction_counit_app, trivial_projective_of_subsingleton, instIsTrivialTrivial, standardComplex.εToSingle₀_comp_eq, barResolution_complex, trivial_ρ_apply, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, standardComplex.quasiIso_forget₂_εToSingle₀, standardComplex.d_comp_ε, FiniteCyclicGroup.resolution_complex, standardComplex.instQuasiIsoNatεToSingle₀, FiniteCyclicGroup.resolution_quasiIso, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, FiniteCyclicGroup.resolution_π, FiniteCyclicGroup.resolution.π_f, trivial_V, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
trivialFunctor 📖	CompOp	11 math math: invariantsAdjunction_homEquiv_symm_apply_hom, instIsTrivialObjModuleCatTrivialFunctor, coinvariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_symm_apply_hom, invariantsAdjunction_unit_app, trivialFunctor_obj_V, coinvariantsAdjunction_unit_app, trivialFunctor_map_hom, invariantsAdjunction_homEquiv_apply_hom, invariantsAdjunction_counit_app, coinvariantsAdjunction_homEquiv_apply_hom
ρ 📖	CompOp	283 math math: invariantsAdjunction_homEquiv_symm_apply_hom, hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, trivial_ρ, MonoidalClosed.linearHomEquiv_symm_hom, groupCohomology.mem_cocycles₂_def, groupCohomology.d₂₃_hom_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, resCoindToHom_hom_apply_coe, groupCohomology.cocyclesIso₀_hom_comp_f, groupHomology.d₃₂_single, coindToInd_of_support_subset_orbit, groupHomology.mapCycles₁_comp_apply, groupCohomology.π_comp_H0Iso_hom, hom_whiskerRight, groupCohomology.H0IsoOfIsTrivial_hom, groupHomology.mem_cycles₂_iff, coindToInd_indToCoind, groupCohomology.d₁₂_hom_apply, groupHomology.mapCycles₁_comp_assoc, add_hom, groupCohomology.d₀₁_hom_apply, groupHomology.d₃₂_single_one_thd, preservesLimits_forget, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, finsuppToCoinvariantsTensorFree_single, hom_surjective, groupHomology.chains₁ToCoinvariantsKer_surjective, standardComplex.d_eq, hom_bijective, groupHomology.π_comp_H0Iso_hom_assoc, groupCohomology.mem_cocycles₁_def, μ_def, hom_id, groupCohomology.mapShortComplexH2_comp_assoc, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, norm_comm_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupHomology.d₂₁_single_inv_mul_ρ_add_single, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupHomology.d₁₀_comp_coinvariantsMk_apply, hom_hom_leftUnitor, ActionToRep_obj_ρ, ihom_ev_app_hom, MonoidalClosed.linearHomEquivComm_hom, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.shortComplexH0_f, Representation.equivOfIso_toFun, standardComplex.εToSingle₀_comp_eq, coindVEquiv_symm_apply_coe, liftHomOfSurj_toLinearMap, instEpiModuleCatAppCoinvariantsMk, forget_map, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, invariantsAdjunction_unit_app, groupHomology.cyclesMap_comp_assoc, tensorHomEquiv_apply, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, coinvariantsFunctor_obj_carrier, applyAsHom_comm_apply, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupHomology.chainsMap_f_single, groupCohomology.subtype_comp_d₀₁_apply, coindFunctorIso_inv_app_hom_toFun_coe, instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupCohomology.cocycles₂_map_one_snd, coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, δ_def, groupCohomology.map_H0Iso_hom_f, indToCoindAux_comm, FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, res_map_hom_toLinearMap, forget_obj, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, ofMulDistribMulAction_ρ_apply_apply, RepToAction_map_hom, groupCohomology.cochainsMap_comp_assoc, ofHom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, groupCohomology.π_comp_H0Iso_hom_apply, subtype_hom_toFun, coinvariantsFunctor_hom_ext_iff, trivial_ρ_apply, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, indToCoindAux_mul_fst, ihom_obj_ρ_apply, smul_hom, mkIso_hom_hom_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, hom_braiding, groupCohomology.mem_cocycles₂_iff, tensor_ρ, groupHomology.d₁₀_comp_coinvariantsMk, hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, hom_injective, ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, Representation.linHom.invariantsEquivRepHom_apply, resCoindHomEquiv_symm_apply, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, zsmul_hom, ofModuleMonoidAlgebra_obj_ρ, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, coinvariantsShortComplex_f, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, inv_hom_apply, nsmul_hom, mkIso_inv_hom_apply, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, coindVEquiv_apply, groupHomology.inhomogeneousChains.d_single, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupCohomology.map_id_comp_H0Iso_hom, indToCoindAux_mul_snd, zero_hom, preservesColimits_forget, hom_inv_rightUnitor, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, hom_hom_rightUnitor, linearization_obj_ρ, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, of_ρ, coe_res_obj_ρ', groupCohomology.cochainsMap_f, inhomogeneousCochains.d_hom_apply, ρ_mul, coind'_ext_iff, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, Representation.equivOfIso_invFun, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, sub_hom, mkIso_inv_hom_toLinearMap, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, standardComplex.quasiIso_forget₂_εToSingle₀, leftRegularHom_hom_single, homEquiv_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, coinvariantsAdjunction_unit_app, coinvariantsMk_app_hom, forget₂_moduleCat_obj, groupCohomology.cocyclesMap_comp_assoc, indCoindIso_hom_hom_toLinearMap, groupHomology.pOpcycles_comp_opcyclesIso_hom, RepToAction_obj_ρ, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, indResHomEquiv_apply, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.δ₀_apply, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, unit_iso_comm, leftRegularHomEquiv_symm_single, indCoindIso_inv_hom_toLinearMap, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.chainsMap_f_hom, forget₂_moduleCat_map, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.map_id_comp_H0Iso_hom_apply, norm_apply, groupCohomology.mapCocycles₁_comp_i_apply, MonoidalClosed.linearHomEquiv_hom, invariantsAdjunction_homEquiv_apply_hom, hom_comm_apply, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, sum_hom, hom_inv_leftUnitor, groupCohomology.cochainsMap_f_hom, standardComplex.d_apply, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.π_comp_H0Iso_hom, hom_inv_associator, quotientToCoinvariantsFunctor_map_hom_toLinearMap, homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, coinvariantsTensorMk_apply, groupHomology.H0π_comp_H0Iso_hom, ihom_map, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, invariantsFunctor_map_hom, id_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, invariantsAdjunction_counit_app, groupHomology.d₂₁_single_one_snd, groupHomology.d₃₂_single_one_snd, coinvariantsTensorIndHom_mk_tmul_indVMk, ihom_coev_app_hom, indToCoind_coindToInd, Representation.linHom.mem_invariants_iff_comm, comp_apply, hom_tensorHom, indResHomEquiv_symm_apply, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupCohomology.subtype_comp_d₀₁, hom_comp, groupHomology.d₁₀_single_inv, res_obj_ρ, hom_whiskerLeft, groupHomology.shortComplexH0_g, RepToAction_obj, applyAsHom_apply, mkQ_hom_toFun, groupHomology.d₂₁_single, groupHomology.inhomogeneousChains.d_eq, epi_iff_surjective, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MonoidalClosed.linearHomEquivComm_symm_hom, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.H0π_comp_H0Iso_hom_assoc, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, groupCohomology.cocyclesMk₀_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, groupHomology.lsingle_comp_chainsMap_f_assoc, tensorHomEquiv_symm_apply, hom_inv_apply, tensorUnit_ρ, groupHomology.single_mem_cycles₂_iff, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, coinvariantsAdjunction_homEquiv_apply_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, ihom_obj_ρ, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, groupCohomology.H1InfRes_f, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, ofHom_apply, groupHomology.single_mem_cycles₁_iff, coinvariantsFunctor_map_hom, groupHomology.d₂₁_single_ρ_add_single_inv_mul, groupCohomology.map_id_comp_H0Iso_hom_assoc, ihom_obj_ρ_def, reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, barComplex.d_single, mono_iff_injective, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, mkIso_hom_hom_toLinearMap, groupHomology.H0π_comp_map_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, groupHomology.mem_cycles₁_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, instIsTrivialVOfCompLinearMapIdρ, neg_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.chainsMap_f, quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, coindFunctorIso_hom_app_hom_toFun_hom_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ActionToRep_map 📖	mathematical	—	CategoryTheory.Functor.map Action ModuleCat ModuleCat.moduleCategory Action.instCategory Rep Ring.toSemiring instCategory ActionToRep ofHom ModuleCat.carrier Action.V ModuleCat.isAddCommGroup ModuleCat.isModule MonoidHom.comp CategoryTheory.End CategoryTheory.Category.toCategoryStruct LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive Module.End.instSemiring RingEquiv.toMonoidHom ModuleCat.endRingEquiv Action.ρ ModuleCat.Hom.hom Action.Hom.hom	—	—
ActionToRep_obj_V 📖	mathematical	—	V Ring.toSemiring CategoryTheory.Functor.obj Action ModuleCat ModuleCat.moduleCategory Action.instCategory Rep instCategory ActionToRep ModuleCat.carrier Action.V	—	—
ActionToRep_obj_ρ 📖	mathematical	—	ρ Ring.toSemiring CategoryTheory.Functor.obj Action ModuleCat ModuleCat.moduleCategory Action.instCategory Rep instCategory ActionToRep MonoidHom.comp CategoryTheory.End CategoryTheory.Category.toCategoryStruct Action.V LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive Module.End.instSemiring RingEquiv.toMonoidHom ModuleCat.endRingEquiv Action.ρ	—	—
RepToAction_map_hom 📖	mathematical	—	Action.Hom.hom ModuleCat ModuleCat.moduleCategory ModuleCat.of V Ring.toSemiring hV1 hV2 MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive RingEquiv.toMonoidHom RingEquiv.symm CategoryTheory.End.mul Module.End.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd LinearMap.instAdd ModuleCat.endRingEquiv ρ CategoryTheory.Functor.map Rep instCategory Action Action.instCategory RepToAction Hom.toModuleCatHom	—	—
RepToAction_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep Ring.toSemiring instCategory Action ModuleCat ModuleCat.moduleCategory Action.instCategory RepToAction ModuleCat.of V hV1 hV2 MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive RingEquiv.toMonoidHom RingEquiv.symm CategoryTheory.End.mul Module.End.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd LinearMap.instAdd ModuleCat.endRingEquiv ρ	—	—
RepToAction_obj_V_carrier 📖	mathematical	—	ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Ring.toSemiring instCategory Action Action.instCategory RepToAction V	—	—
RepToAction_obj_V_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Ring.toSemiring instCategory Action Action.instCategory RepToAction hV1	—	—
RepToAction_obj_V_isModule 📖	mathematical	—	ModuleCat.isModule Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Ring.toSemiring instCategory Action Action.instCategory RepToAction hV2	—	—
RepToAction_obj_ρ 📖	mathematical	—	Action.ρ ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Ring.toSemiring instCategory Action Action.instCategory RepToAction MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.of V hV1 hV2 AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive RingEquiv.toMonoidHom RingEquiv.symm CategoryTheory.End.mul Module.End.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd LinearMap.instAdd ModuleCat.endRingEquiv ρ	—	—
add_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver instAddHom	—	hom_ext Representation.IntertwiningMap.add_comp
add_hom 📖	mathematical	—	Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instAdd	—	—
applyAsHom_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V CommMonoid.toMonoid AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom applyAsHom LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—
applyAsHom_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommMonoid.toMonoid CategoryTheory.Category.toCategoryStruct instCategory applyAsHom	—	hom_ext Representation.IntertwiningMap.ext LinearMap.ext hom_comm_apply
applyAsHom_comm_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V CommMonoid.toMonoid AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike CategoryTheory.ConcreteCategory.hom Rep instCategory instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise applyAsHom_comm
applyAsHom_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommMonoid.toMonoid CategoryTheory.Category.toCategoryStruct instCategory applyAsHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' applyAsHom_comm
comp_add 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver instAddHom	—	hom_ext Representation.IntertwiningMap.comp_add
comp_apply 📖	mathematical	—	DFunLike.coe V CategoryTheory.ConcreteCategory.hom Rep instCategory Representation.IntertwiningMap AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
comp_smul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Category.toCategoryStruct instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver instSMulHom	—	hom_ext Representation.IntertwiningMap.ext LinearMap.ext smulCommClass_self RingHomCompTriple.ids Representation.IntertwiningMap.smul_comp
epi_iff_surjective 📖	mathematical	—	CategoryTheory.Epi Rep Ring.toSemiring instCategory V DFunLike.coe Representation.IntertwiningMap AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom	—	ModuleCat.epi_iff_surjective CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits preservesColimits_forget CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier
finsupp_V 📖	mathematical	—	V CommSemiring.toSemiring CommRing.toCommSemiring finsupp Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid hV1	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map Rep instCategory CategoryTheory.types CategoryTheory.forget Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep instCategory CategoryTheory.types CategoryTheory.forget Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ	—	—
forget₂_moduleCat_map 📖	mathematical	—	CategoryTheory.Functor.map Rep Ring.toSemiring instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat ModuleCat.ofHom Representation.IntertwiningMap.toLinearMap Hom.hom	—	—
forget₂_moduleCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep Ring.toSemiring instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat ModuleCat.of	—	—
free_ext 📖	—	DFunLike.coe Representation.IntertwiningMap V CommSemiring.toSemiring CommRing.toCommSemiring free AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instZero MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	LinearEquiv.injective RingHomInvPair.ids
homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ EquivLike.toFunLike Equiv.instEquivLike homEquiv Hom.hom	—	—
homEquiv_def 📖	mathematical	—	CategoryTheory.Adjunction.homEquiv Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.MonoidalCategory.tensorLeft instMonoidalCategory CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed instMonoidalClosed CategoryTheory.ihom.adjunction tensorHomEquiv	—	CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv ofHom	—	—
hom_bijective 📖	mathematical	—	Function.Bijective Hom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom	—	hom_ext hom_ofHom
hom_braiding 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instBraidedCategory Representation.Equiv.toIntertwiningMap TensorProduct V AddCommGroup.toAddCommMonoid hV1 hV2 TensorProduct.addCommMonoid TensorProduct.instModule Representation.tprod ρ Representation.TensorProduct.comm	—	—
hom_comm_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	RingHomCompTriple.ids Representation.IntertwiningMap.isIntertwining'
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct instCategory Representation.IntertwiningMap.comp V AddCommGroup.toAddCommMonoid hV1 hV2 ρ	—	—
hom_comp_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct instCategory LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_hom_associator 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator Representation.Equiv.toIntertwiningMap TensorProduct V AddCommGroup.toAddCommMonoid hV1 hV2 TensorProduct.addCommMonoid TensorProduct.instModule Representation.tprod ρ Representation.TensorProduct.assoc	—	Representation.IntertwiningMap.ext TensorProduct.ext_threefold
hom_hom_leftUnitor 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor Representation.Equiv.toIntertwiningMap TensorProduct V NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid hV1 Semiring.toModule hV2 TensorProduct.addCommMonoid TensorProduct.instModule Representation.tprod Representation.trivial ρ Representation.TensorProduct.lid	—	—
hom_hom_rightUnitor 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor Representation.Equiv.toIntertwiningMap TensorProduct V AddCommGroup.toAddCommMonoid hV1 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring hV2 Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule Representation.tprod ρ Representation.trivial Representation.TensorProduct.rid	—	—
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id Rep CategoryTheory.Category.toCategoryStruct instCategory Representation.IntertwiningMap.id V AddCommGroup.toAddCommMonoid hV1 hV2 ρ	—	—
hom_injective 📖	mathematical	—	Hom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom	—	Function.Bijective.injective hom_bijective
hom_inv_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom CategoryTheory.Iso.hom Rep instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_inv_associator 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator Representation.Equiv.toIntertwiningMap TensorProduct V AddCommGroup.toAddCommMonoid hV1 hV2 TensorProduct.addCommMonoid TensorProduct.instModule Representation.tprod ρ Representation.Equiv.symm Representation.TensorProduct.assoc	—	—
hom_inv_leftUnitor 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor Representation.Equiv.toIntertwiningMap V TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid hV1 Semiring.toModule hV2 TensorProduct.addCommMonoid TensorProduct.instModule ρ Representation.tprod Representation.trivial Representation.Equiv.symm Representation.TensorProduct.lid	—	—
hom_inv_rightUnitor 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor Representation.Equiv.toIntertwiningMap V TensorProduct AddCommGroup.toAddCommMonoid hV1 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring hV2 Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule ρ Representation.tprod Representation.trivial Representation.Equiv.symm Representation.TensorProduct.rid	—	—
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
hom_surjective 📖	mathematical	—	Hom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom	—	Function.Bijective.surjective hom_bijective
hom_tensorHom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom Representation.IntertwiningMap.tensor V AddCommGroup.toAddCommMonoid hV1 hV2 ρ	—	—
hom_whiskerLeft 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft Representation.IntertwiningMap.lTensor V AddCommGroup.toAddCommMonoid hV1 hV2 ρ	—	—
hom_whiskerRight 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight Representation.IntertwiningMap.rTensor V AddCommGroup.toAddCommMonoid hV1 hV2 ρ	—	—
id_apply 📖	mathematical	—	DFunLike.coe V CategoryTheory.ConcreteCategory.hom Rep instCategory Representation.IntertwiningMap AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ihom_coev_app_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft instMonoidalCategory CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed instMonoidalClosed AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom CategoryTheory.NatTrans.app CategoryTheory.ihom.coev LinearMap.flip TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid RingHom.id Semiring.toNonAssocSemiring	—	LinearMap.ext TensorProduct.smulCommClass_left smulCommClass_self
ihom_ev_app_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep instCategory CategoryTheory.Functor.comp CategoryTheory.ihom instMonoidalCategory CategoryTheory.MonoidalClosed.closed instMonoidalClosed CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom CategoryTheory.NatTrans.app CategoryTheory.ihom.ev DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing CommSemiring.toCommMonoid TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike TensorProduct.uncurry LinearMap.flip LinearMap.id	—	LinearMap.ext smulCommClass_self LinearMap.instSMulCommClass
ihom_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ihom ofHom LinearMap RingHom.id Semiring.toNonAssocSemiring V AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.addCommGroup LinearMap.module Representation.linHom ρ DFunLike.coe LinearMap.addCommMonoid LinearMap.instFunLike LinearMap.llcomp Representation.IntertwiningMap.toLinearMap Hom.hom	—	—
ihom_obj_V 📖	mathematical	—	V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep instCategory ihom LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid hV1 hV2	—	—
ihom_obj_ρ 📖	mathematical	—	ρ CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep instCategory ihom Representation.linHom V AddCommGroup.toAddCommMonoid hV1 hV2	—	smulCommClass_self
ihom_obj_ρ_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ CategoryTheory.Functor.obj Rep instCategory ihom LinearMap.comp RingHomCompTriple.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smulCommClass_self
ihom_obj_ρ_def 📖	mathematical	—	ρ CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep instCategory CategoryTheory.ihom instMonoidalCategory CategoryTheory.MonoidalClosed.closed instMonoidalClosed ihom	—	—
instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier 📖	mathematical	—	CategoryTheory.Functor.Additive Rep Ring.toSemiring ModuleCat instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat	—	ModuleCat.hom_ext
instEpiModuleCatToModuleCatHom 📖	mathematical	—	CategoryTheory.Epi ModuleCat ModuleCat.moduleCategory ModuleCat.of V Ring.toSemiring hV1 hV2 Hom.toModuleCatHom	—	—
instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier 📖	mathematical	—	CategoryTheory.Functor.Faithful Rep Ring.toSemiring instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat	—	CategoryTheory.forget₂_faithful
instIsEquivalenceActionModuleCatActionToRep 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence Action ModuleCat ModuleCat.moduleCategory Action.instCategory Rep Ring.toSemiring instCategory ActionToRep	—	CategoryTheory.Equivalence.isEquivalence_inverse
instIsEquivalenceActionModuleCatRepToAction 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence Rep Ring.toSemiring instCategory Action ModuleCat ModuleCat.moduleCategory Action.instCategory RepToAction	—	CategoryTheory.Equivalence.isEquivalence_functor
instIsTrivialObjModuleCatTrivialFunctor 📖	mathematical	—	IsTrivial CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory Rep Ring.toSemiring instCategory trivialFunctor	—	—
instIsTrivialOfOfIsTrivial 📖	mathematical	—	IsTrivial of Ring.toSemiring	—	Representation.isTrivial_def
instIsTrivialTrivial 📖	mathematical	—	IsTrivial trivial Ring.toSemiring	—	Representation.isTrivial_def Representation.instIsTrivialTrivial
instIsTrivialVOfCompLinearMapIdρ 📖	mathematical	—	Representation.IsTrivial V Ring.toSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid of AddCommGroup.toAddCommMonoid hV1 hV2 MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive instLinear ModuleCat.instLinear CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat	—	ModuleCat.hom_ext LinearMap.ext
instMonoModuleCatToModuleCatHom 📖	mathematical	—	CategoryTheory.Mono ModuleCat ModuleCat.moduleCategory ModuleCat.of V Ring.toSemiring hV1 hV2 Hom.toModuleCatHom	—	—
instMonoidalLinear 📖	mathematical	—	CategoryTheory.MonoidalLinear CommSemiring.toSemiring CommRing.toCommSemiring Rep instCategory instPreadditive instLinear instMonoidalCategory instMonoidalPreadditive	—	instMonoidalPreadditive hom_ext Representation.IntertwiningMap.lTensor_smul Representation.IntertwiningMap.rTensor_smul
instMonoidalPreadditive 📖	mathematical	—	CategoryTheory.MonoidalPreadditive Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory instPreadditive instMonoidalCategory	—	hom_ext Representation.IntertwiningMap.lTensor_zero Representation.IntertwiningMap.rTensor_zero Representation.IntertwiningMap.lTensor_add Representation.IntertwiningMap.rTensor_add
inv_hom_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom CategoryTheory.Iso.inv Rep instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
leftRegularHomEquiv_symm_single 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V Ring.toSemiring CommRing.toRing leftRegular AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddCommGroupHom instModuleHom EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm leftRegularHomEquiv Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne LinearMap LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	RingHomInvPair.ids Finsupp.sum_single_index zero_smul one_smul
leftRegularHom_hom_single 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V Ring.toSemiring leftRegular AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom leftRegularHom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap RingHom.id LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	Finsupp.sum_single_index zero_smul
linearization_map 📖	mathematical	—	CategoryTheory.Functor.map Action CategoryTheory.types Action.instCategory Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory linearization ofHom Finsupp Action.V MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Representation.linearize Representation.linearizeMap	—	—
linearization_obj_V 📖	mathematical	—	V CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep instCategory linearization Finsupp Action.V MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
linearization_obj_ρ 📖	mathematical	—	ρ CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep instCategory linearization Representation.linearize	—	—
mkIso_hom_hom 📖	mathematical	—	Hom.hom of CategoryTheory.Iso.hom Rep instCategory mkIso Representation.Equiv.toIntertwiningMap AddCommGroup.toAddCommMonoid	—	—
mkIso_hom_hom_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V of AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom CategoryTheory.Iso.hom Rep instCategory mkIso LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation.IntertwiningMap.toLinearMap Representation.Equiv.toIntertwiningMap	—	—
mkIso_hom_hom_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V of AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom CategoryTheory.Iso.hom Rep instCategory mkIso Representation.Equiv.toIntertwiningMap	—	—
mkIso_inv_hom_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V of AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom CategoryTheory.Iso.inv Rep instCategory mkIso Representation.Equiv EquivLike.toFunLike Representation.Equiv.instEquivLike Representation.Equiv.symm	—	—
mkIso_inv_hom_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V of AddCommGroup.toAddCommMonoid hV1 hV2 ρ Hom.hom CategoryTheory.Iso.inv Rep instCategory mkIso Representation.Equiv.toIntertwiningMap Representation.Equiv.symm	—	—
mkQ_hom_toFun 📖	mathematical	Submodule V Ring.toSemiring CommMonoid.toMonoid AddCommGroup.toAddCommMonoid hV1 hV2 Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	DFunLike.coe Representation.IntertwiningMap V Ring.toSemiring CommMonoid.toMonoid HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid hV1 hV2 Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module ρ Representation.quotient Representation.IntertwiningMap.instFunLike Hom.hom quotient mkQ	—	—
mono_iff_injective 📖	mathematical	—	CategoryTheory.Mono Rep Ring.toSemiring instCategory V DFunLike.coe Representation.IntertwiningMap AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom	—	ModuleCat.mono_iff_injective CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits preservesLimits_forget CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier
neg_hom 📖	mathematical	—	Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instNeg	—	—
normNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Functor.id normNatTrans norm	—	—
norm_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike Hom.hom norm Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Representation.norm	—	—
norm_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Category.toCategoryStruct instCategory norm	—	hom_ext Representation.IntertwiningMap.ext LinearMap.ext LinearMap.coe_sum Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Representation.IntertwiningMap.instLinearMapClass Finset.sum_congr hom_comm_apply
norm_comm_apply 📖	mathematical	—	DFunLike.coe Module.End V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Representation.norm ρ Representation.IntertwiningMap Representation.IntertwiningMap.instFunLike CategoryTheory.ConcreteCategory.hom Rep instCategory instConcreteCategoryIntertwiningMapVρ	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise norm_comm
norm_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Category.toCategoryStruct instCategory norm	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' norm_comm
nsmul_hom 📖	mathematical	—	Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSMulNatHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instSMulNat	—	—
ofDistribMulAction_ρ_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring V ofDistribMulAction AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
ofHom_add 📖	mathematical	—	ofHom Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instAdd Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instAddHom	—	—
ofHom_apply 📖	mathematical	—	DFunLike.coe of V CategoryTheory.ConcreteCategory.hom Rep instCategory Representation.IntertwiningMap AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom Representation.IntertwiningMap.comp AddCommGroup.toAddCommMonoid CategoryTheory.CategoryStruct.comp Rep CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom V hV1 hV2 ρ Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom Representation.IntertwiningMap.id AddCommGroup.toAddCommMonoid CategoryTheory.CategoryStruct.id Rep CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_neg 📖	mathematical	—	ofHom Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instNeg Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instNegHom	—	—
ofHom_nsmul 📖	mathematical	—	ofHom Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instSMulNat Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instSMulNatHom	—	—
ofHom_smul 📖	mathematical	—	ofHom CommSemiring.toSemiring CommRing.toCommSemiring Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instSMul Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instSMulHom	—	—
ofHom_sub 📖	mathematical	—	ofHom Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instSub Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instSubHom	—	—
ofHom_sum 📖	mathematical	—	ofHom Finset.sum Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instAddCommMonoid Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instAddCommGroupHom	—	Finset.induction Finset.sum_insert
ofHom_zero 📖	mathematical	—	ofHom Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instZero Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instZeroHom	—	—
ofHom_zsmul 📖	mathematical	—	ofHom Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Representation.IntertwiningMap.instSMulInt Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory of instSMulIntHom	—	—
ofMulDistribMulAction_ρ_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring V ofMulDistribMulAction AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Additive.toMul	—	—
of_V 📖	mathematical	—	V of	—	—
of_tensor 📖	mathematical	—	of CommSemiring.toSemiring CommRing.toCommSemiring TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
of_ρ 📖	mathematical	—	ρ of	—	—
preservesColimits_forget 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize Rep Ring.toSemiring instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat	—	CategoryTheory.Limits.preservesColimits_of_natIso CategoryTheory.Limits.comp_preservesColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence instIsEquivalenceActionModuleCatRepToAction Action.preservesColimits_forget ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self
preservesLimits_forget 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize Rep Ring.toSemiring instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModuleCat	—	CategoryTheory.Limits.preservesLimits_of_natIso CategoryTheory.Limits.comp_preservesLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence instIsEquivalenceActionModuleCatRepToAction Action.preservesLimits_forget ModuleCat.instHasLimitsOfSize
reflectsIsomorphisms_forget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Rep instCategory CategoryTheory.types CategoryTheory.forget Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instFunLike instConcreteCategoryIntertwiningMapVρ	—	Equiv.left_inv Equiv.right_inv CategoryTheory.Iso.isIso_hom
smul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Category.toCategoryStruct instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver instSMulHom	—	hom_ext Representation.IntertwiningMap.comp_smul
smul_hom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSMulHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instSMul	—	—
sub_hom 📖	mathematical	—	Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instSub	—	—
subtype_hom_toFun 📖	mathematical	Submodule V Ring.toSemiring CommMonoid.toMonoid AddCommGroup.toAddCommMonoid hV1 hV2 Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	DFunLike.coe Representation.IntertwiningMap V Ring.toSemiring CommMonoid.toMonoid Submodule AddCommGroup.toAddCommMonoid hV1 hV2 SetLike.instMembership Submodule.setLike Submodule.addCommGroup Submodule.module Representation.subrepresentation ρ Representation.IntertwiningMap.instFunLike Hom.hom subrepresentation subtype	—	—
sum_hom 📖	mathematical	—	Hom.hom Finset.sum Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommGroup.toAddCommMonoid instAddCommGroupHom Representation.IntertwiningMap V hV1 hV2 ρ Representation.IntertwiningMap.instAddCommMonoid	—	Finset.induction Finset.sum_insert
tensorHomEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.obj ihom EquivLike.toFunLike Equiv.instEquivLike tensorHomEquiv ofHom V LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.addCommGroup LinearMap.module ρ Representation.linHom LinearMap.flip TensorProduct.curry Representation.IntertwiningMap.toLinearMap Hom.hom	—	—
tensorHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorHomEquiv ofHom TensorProduct V AddCommGroup.toAddCommMonoid hV1 hV2 TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod ρ LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module TensorProduct.addCommMonoid LinearMap.instFunLike TensorProduct.uncurry LinearMap.flip Representation.IntertwiningMap.toLinearMap Hom.hom	—	—
tensorUnit_V 📖	mathematical	—	V CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorUnit Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
tensorUnit_ρ 📖	mathematical	—	ρ CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorUnit Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Representation.trivial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—
tensor_V 📖	mathematical	—	V CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory TensorProduct AddCommGroup.toAddCommMonoid hV1 hV2	—	—
tensor_ρ 📖	mathematical	—	ρ CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Representation.tprod V AddCommGroup.toAddCommMonoid hV1 hV2	—	—
toAdditive_apply 📖	mathematical	—	DFunLike.coe AddEquiv V Int.instSemiring ofMulDistribMulAction Additive AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid hV1 Additive.add MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup EquivLike.toFunLike AddEquiv.instEquivLike toAdditive	—	—
toAdditive_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv Additive V Int.instSemiring ofMulDistribMulAction Additive.add MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid hV1 EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAdditive	—	—
trivialFunctor_map_hom 📖	mathematical	—	Hom.hom Ring.toSemiring of ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Representation.trivial AddCommGroup.toAddCommMonoid CategoryTheory.Functor.map ModuleCat ModuleCat.moduleCategory Rep instCategory trivialFunctor ModuleCat.Hom.hom	—	—
trivialFunctor_obj_V 📖	mathematical	—	V Ring.toSemiring CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory Rep instCategory trivialFunctor ModuleCat.carrier	—	—
trivial_V 📖	mathematical	—	V trivial	—	—
trivial_ρ 📖	mathematical	—	DFunLike.coe Representation V trivial AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ LinearMap.id	—	—
trivial_ρ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring V trivial AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
zero_hom 📖	mathematical	—	Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instZero	—	—
zsmul_hom 📖	mathematical	—	Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSMulIntHom Representation.IntertwiningMap V AddCommGroup.toAddCommMonoid hV1 hV2 ρ Representation.IntertwiningMap.instSMulInt	—	—
δ_def 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ Action CategoryTheory.types Action.instCategory Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory instMonoidalCategory linearization CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalActionTypeLinearization ofHom Finsupp Action.V CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct V CategoryTheory.Functor.obj AddCommGroup.toAddCommMonoid hV1 hV2 Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.addCommGroup Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule TensorProduct.instModule Representation.linearize Representation.tprod ρ Representation.LinearizeMonoidal.δ	—	—
δ_hom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep instCategory linearization CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory instMonoidalCategory CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalActionTypeLinearization Representation.LinearizeMonoidal.δ	—	—
ε_def 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε Action CategoryTheory.types Action.instCategory Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory instMonoidalCategory linearization CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalActionTypeLinearization ofHom Finsupp Action.V CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toAddCommGroup CommRing.toRing Finsupp.instAddCommGroup Semiring.toModule Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Representation.trivial Representation.linearize Representation.LinearizeMonoidal.ε	—	—
ε_hom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorUnit Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory linearization Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalActionTypeLinearization Representation.LinearizeMonoidal.ε	—	—
η_def 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η Action CategoryTheory.types Action.instCategory Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory instMonoidalCategory linearization CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalActionTypeLinearization ofHom Finsupp Action.V CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Representation.linearize Representation.trivial Representation.LinearizeMonoidal.η	—	—
η_hom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep instCategory linearization CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory instMonoidalCategory CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalActionTypeLinearization Representation.LinearizeMonoidal.η	—	—
μ_def 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ Action CategoryTheory.types Action.instCategory Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory instMonoidalCategory linearization CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalActionTypeLinearization ofHom TensorProduct V CategoryTheory.Functor.obj AddCommGroup.toAddCommMonoid hV1 hV2 Finsupp Action.V CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Representation.tprod ρ Representation.linearize Representation.LinearizeMonoidal.μ	—	—
μ_hom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Rep instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory linearization Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalActionTypeLinearization Representation.LinearizeMonoidal.μ	—	—
ρ_mul 📖	mathematical	—	DFunLike.coe Representation V AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ MulOne.toMul LinearMap.comp RingHomCompTriple.ids	—	LinearMap.ext RingHomCompTriple.ids map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass

Rep.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	134 math math: Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Rep.hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, Rep.μ_hom, Rep.MonoidalClosed.linearHomEquiv_symm_hom, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, Rep.resCoindToHom_hom_apply_coe, groupHomology.mapCycles₁_comp_apply, Rep.hom_whiskerRight, Rep.hom_ofHom, groupHomology.mapCycles₁_comp_assoc, Rep.add_hom, groupCohomology.map_H0Iso_hom_f_apply, Rep.hom_surjective, Rep.standardComplex.d_eq, Rep.hom_bijective, Rep.hom_id, groupCohomology.mapShortComplexH2_comp_assoc, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, Rep.hom_hom_leftUnitor, Rep.ihom_ev_app_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, Rep.coindVEquiv_symm_apply_coe, Rep.liftHomOfSurj_toLinearMap, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.cyclesMap_comp_assoc, Rep.tensorHomEquiv_apply, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, groupHomology.chainsMap_f_single, Rep.coindFunctorIso_inv_app_hom_toFun_coe, Rep.indToCoindAux_comm, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, Rep.res_map_hom_toLinearMap, groupCohomology.cochainsMap_comp_assoc, Rep.ofHom_hom, groupHomology.mapCycles₁_comp_i_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, Rep.subtype_hom_toFun, Rep.smul_hom, Rep.mkIso_hom_hom_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, Rep.hom_braiding, Rep.hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, Rep.hom_injective, Rep.resCoindHomEquiv_symm_apply, Rep.zsmul_hom, Rep.inv_hom_apply, Rep.nsmul_hom, Rep.mkIso_inv_hom_apply, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupCohomology.map_id_comp_H0Iso_hom_apply, groupHomology.chainsMap_id_f_hom_eq_mapRange, Rep.zero_hom, Rep.δ_hom, Rep.hom_inv_rightUnitor, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.hom_hom_rightUnitor, groupHomology.lsingle_comp_chainsMap_f, groupCohomology.cochainsMap_f, Rep.coind'_ext_iff, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Rep.sub_hom, Rep.ε_hom, Rep.mkIso_inv_hom_toLinearMap, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, Rep.leftRegularHom_hom_single, Rep.homEquiv_apply, groupCohomology.cocyclesMap_comp_assoc, Rep.indCoindIso_hom_hom_toLinearMap, Rep.hom_ext_iff, Rep.trivialFunctor_map_hom, Rep.η_hom, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, Rep.indResHomEquiv_apply, Rep.leftRegularHomEquiv_symm_single, Rep.indCoindIso_inv_hom_toLinearMap, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.chainsMap_f_hom, Rep.forget₂_moduleCat_map, groupHomology.map_id_comp_H0Iso_hom_apply, Rep.norm_apply, groupCohomology.mapCocycles₁_comp_i_apply, Rep.mkIso_hom_hom, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.hom_comm_apply, Rep.sum_hom, Rep.hom_inv_leftUnitor, groupCohomology.cochainsMap_f_hom, Rep.standardComplex.d_apply, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, Rep.hom_inv_associator, Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.mapShortComplexH1_comp_assoc, Rep.ihom_map, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, Rep.invariantsFunctor_map_hom, Rep.ihom_coev_app_hom, Rep.hom_tensorHom, Rep.indResHomEquiv_symm_apply, groupHomology.mapCycles₂_comp_i_apply, Rep.hom_comp, Rep.hom_whiskerLeft, Rep.applyAsHom_apply, Rep.mkQ_hom_toFun, Rep.epi_iff_surjective, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.lsingle_comp_chainsMap_f_assoc, Rep.tensorHomEquiv_symm_apply, Rep.hom_inv_apply, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, Rep.coinvariantsAdjunction_homEquiv_apply_hom, Rep.coinvariantsFunctor_map_hom, Rep.barComplex.d_single, Rep.mono_iff_injective, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, Rep.mkIso_hom_hom_toLinearMap, groupHomology.H0π_comp_map_apply, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, Rep.neg_hom, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun
hom' 📖	CompOp	1 math math: ext_iff
toModuleCatHom 📖	CompOp	19 math math: groupHomology.H0π_comp_map, groupCohomology.map_H0Iso_hom_f, Rep.RepToAction_map_hom, groupHomology.H0π_comp_map_assoc, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, Rep.instEpiModuleCatToModuleCatHom, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, groupHomology.cyclesIso₀_inv_comp_cyclesMap, Rep.instMonoModuleCatToModuleCatHom, groupHomology.mapShortComplexH1_τ₃, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, groupCohomology.mapShortComplexH1_τ₁, groupHomology.chainsMap_f_0_comp_chainsIso₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

Rep.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

Rep.MonoidalClosed

Definitions

Name	Category	Theorems
linearHomEquiv 📖	CompOp	2 math math: linearHomEquiv_symm_hom, linearHomEquiv_hom
linearHomEquivComm 📖	CompOp	2 math math: linearHomEquivComm_hom, linearHomEquivComm_symm_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearHomEquivComm_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Rep.instCategory CategoryTheory.ihom Rep.instMonoidalCategory CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Rep.Hom.hom DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Rep.instAddCommGroupHom Rep.instModuleHom EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearHomEquivComm TensorProduct.curry	—	RingHomInvPair.ids
linearHomEquivComm_symm_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Rep.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Rep.instMonoidalCategory AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Rep.Hom.hom DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed Rep.instAddCommGroupHom Rep.instModuleHom EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearHomEquivComm LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike TensorProduct.uncurry	—	TensorProduct.ext' RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass
linearHomEquiv_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Rep.instCategory CategoryTheory.ihom Rep.instMonoidalCategory CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Rep.Hom.hom DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Rep.instAddCommGroupHom Rep.instModuleHom EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearHomEquiv LinearMap.flip smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.curry	—	RingHomInvPair.ids
linearHomEquiv_symm_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Rep.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Rep.instMonoidalCategory AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Rep.Hom.hom DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed Rep.instAddCommGroupHom Rep.instModuleHom EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearHomEquiv LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike TensorProduct.uncurry LinearMap.flip	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Rep.homEquiv_def

Representation

Definitions

Name	Category	Theorems
equivOfIso 📖	CompOp	2 math math: equivOfIso_toFun, equivOfIso_invFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivOfIso_invFun 📖	mathematical	—	Equiv.invFun Rep.V AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ equivOfIso DFunLike.coe CategoryTheory.ConcreteCategory.hom Rep Rep.instCategory IntertwiningMap IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ CategoryTheory.Iso.inv	—	—
equivOfIso_toFun 📖	mathematical	—	DFunLike.coe Equiv Rep.V AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ EquivLike.toFunLike Equiv.instEquivLike equivOfIso CategoryTheory.ConcreteCategory.hom Rep Rep.instCategory IntertwiningMap IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ CategoryTheory.Iso.hom	—	—

(root)

Definitions

Name	Category	Theorems
Rep 📖	CompData	384 math math: Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Rep.hom_hom_associator, groupHomology.mapCycles₂_comp_assoc, Rep.μ_hom, Rep.MonoidalClosed.linearHomEquiv_symm_hom, groupHomology.map₁_quotientGroupMk'_epi, groupHomology.coinfNatTrans_app, groupHomology.mapShortComplexH2_id, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, Rep.ofHom_sub, groupCohomology.δ_apply, groupCohomology.cocyclesMap_id_comp_assoc, groupHomology.mono_δ_of_isZero, Rep.coindResAdjunction_counit_app, Rep.ihom_obj_V, groupHomology.mapCycles₁_comp_apply, groupHomology.mapShortComplexH1_zero, Rep.hom_whiskerRight, groupHomology.cyclesMap_id_comp, Rep.indFunctor_obj, groupHomology.mapShortComplexH2_zero, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, Rep.indCoindNatIso_hom_app, groupHomology.chainsMap_id, Rep.invariantsFunctor_obj_carrier, Rep.barComplex.d_def, Rep.full_res, Rep.instAdditiveResFunctor, Rep.coindFunctor_map, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, Rep.instIsRightAdjointCoindFunctor, groupHomology.mapCycles₁_comp_assoc, Rep.add_hom, Rep.instIsTrivialObjModuleCatTrivialFunctor, Rep.coinvariantsAdjunction_counit_app, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, groupHomology.map_id, groupCohomology.cochainsMap_comp, groupHomology.δ₀_apply, Rep.preservesLimits_forget, groupHomology.coresNatTrans_app, Rep.instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, Rep.of_tensor, Rep.ε_def, groupCohomology.congr, Rep.standardComplex.d_eq, Rep.ofHom_comp, groupHomology.π_comp_H0Iso_hom_assoc, Rep.trivial_projective_of_subsingleton, Rep.μ_def, Rep.hom_id, groupCohomology.mapShortComplexH2_comp_assoc, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, Rep.norm_comm_apply, Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom, Rep.free_projective, groupHomology.d₁₀_comp_coinvariantsMk_apply, groupHomology.mapCycles₁_id_comp_assoc, Rep.hom_hom_leftUnitor, Rep.instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra, Rep.ActionToRep_obj_ρ, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, Rep.instLinearModuleCatObjFunctorCoinvariantsTensor, groupHomology.mapCycles₁_comp, groupHomology.map_comp, Rep.ihom_ev_app_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, Rep.instIsRightAdjointModuleCatInvariantsFunctor, groupCohomology.map_comp, groupHomology.map_id_comp, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Rep.coinvariantsTensorIndIso_inv, groupHomology.functor_obj, Rep.ActionToRep_obj_V, Representation.equivOfIso_toFun, Rep.standardComplex.εToSingle₀_comp_eq, Rep.coindVEquiv_symm_apply_coe, Rep.instEpiModuleCatAppCoinvariantsMk, Rep.homEquiv_def, Rep.ofHom_add, Rep.forget_map, Rep.instHasFiniteProducts, Rep.ofModuleMonoidAlgebra_obj_coe, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, Rep.invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, Rep.diagonal_succ_projective, groupHomology.cyclesMap_comp_assoc, Rep.tensorHomEquiv_apply, Rep.coinvariantsFunctor_obj_carrier, Rep.applyAsHom_comm_apply, Rep.coindFunctorIso_inv_app_hom_toFun_coe, Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, Rep.instProjective, groupCohomology.δ₁_apply, Rep.coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, Rep.δ_def, Rep.coinvariantsTensorIndIso_hom, Rep.barResolution_complex, groupCohomology.cochainsMap_zero, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, Rep.coinvariantsTensorIndNatIso_inv_app, Rep.res_map_hom_toLinearMap, groupHomology.epi_δ_of_isZero, groupHomology.map_chainsFunctor_shortExact, Rep.forget_obj, Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor, Rep.coindResAdjunction_unit_app, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.epi_δ_of_isZero, groupCohomology.cochainsMap_id_comp, groupCohomology.map_id, groupCohomology.mapShortComplexH2_comp, Rep.RepToAction_map_hom, groupCohomology.cochainsMap_comp_assoc, Rep.instIsRightAdjointResFunctor, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, Rep.resIndAdjunction_homEquiv_symm_apply, Rep.coinvariantsFunctor_hom_ext_iff, Rep.instLinearModuleCatCoinvariantsFunctor, Rep.normNatTrans_app, groupHomology.π_comp_H0Iso_hom_apply, Rep.applyAsHom_comm_assoc, groupHomology.chainsFunctor_obj, Rep.instEnoughProjectives, groupCohomology.functor_obj, groupCohomology.cocyclesMap_comp, Rep.ihom_obj_ρ_apply, Rep.RepToAction_obj_V_isAddCommGroup, Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor, Rep.smul_hom, Rep.mkIso_hom_hom_apply, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, Rep.smul_comp, groupCohomology.resNatTrans_app, Rep.hom_braiding, groupCohomology.mapShortComplexH2_zero, Rep.tensor_ρ, Rep.resIndAdjunction_homEquiv_apply, groupHomology.d₁₀_comp_coinvariantsMk, Rep.hom_comp_toLinearMap, groupHomology.mapCycles₂_comp_apply, Representation.linHom.invariantsEquivRepHom_apply, Rep.resCoindHomEquiv_symm_apply, groupHomology.chainsMap_id_comp, groupCohomology.mapShortComplexH1_id, Rep.coinvariantsShortComplex_g, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, Rep.zsmul_hom, Rep.coindResAdjunction_homEquiv_apply, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, Rep.Tor_map, Rep.ofModuleMonoidAlgebra_obj_ρ, Rep.coinvariantsShortComplex_f, Rep.resIndAdjunction_counit_app, Rep.inv_hom_apply, Rep.nsmul_hom, Rep.instLinearResFunctor, Rep.mkIso_inv_hom_apply, Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor, Rep.coindVEquiv_apply, Rep.instMonoidalPreadditive, Rep.ActionToRep_map, Representation.coind'_apply_apply, groupHomology.map_id_comp_H0Iso_hom_assoc, Rep.RepToAction_obj_V_carrier, Rep.RepToAction_obj_V_isModule, groupCohomology.mapShortComplexH2_id_comp_assoc, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.mapShortComplexH2_comp, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.mapCycles₁_id_comp, Rep.trivialFunctor_obj_V, Rep.zero_hom, Rep.δ_hom, Rep.preservesColimits_forget, Rep.ofHom_nsmul, Rep.hom_inv_rightUnitor, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.hom_hom_rightUnitor, Rep.linearization_obj_ρ, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, groupHomology.chainsMap_comp, Rep.instLinearModuleCatInvariantsFunctor, Representation.equivOfIso_invFun, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, groupCohomology.map_id_comp_assoc, Rep.sub_hom, Rep.ε_hom, Rep.isZero_Tor_succ_of_projective, Rep.mkIso_inv_hom_toLinearMap, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, Rep.coinvariantsTensorIndNatIso_hom_app, groupHomology.congr, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, Rep.applyAsHom_comm, Rep.homEquiv_apply, Rep.coinvariantsAdjunction_unit_app, groupCohomology.H1InfRes_g, Rep.standardComplex.d_comp_ε, groupHomology.δ_apply, Rep.coinvariantsMk_app_hom, Rep.indCoindNatIso_inv_app, Rep.instIsEquivalenceActionModuleCatRepToAction, Rep.forget₂_moduleCat_obj, groupCohomology.mapShortComplexH1_id_comp, groupCohomology.cocyclesMap_comp_assoc, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, Rep.coindResAdjunction_homEquiv_symm_apply, Rep.indCoindIso_hom_hom_toLinearMap, groupCohomology.mapShortComplexH1_comp, groupHomology.pOpcycles_comp_opcyclesIso_hom, Rep.trivialFunctor_map_hom, Rep.η_hom, Rep.RepToAction_obj_ρ, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.mapShortComplexH1_id, groupCohomology.map_id_comp, Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, Rep.coinvariantsTensor_hom_ext_iff, Rep.indResHomEquiv_apply, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, groupCohomology.δ₀_apply, Rep.unit_iso_comm, Rep.linearization_map, Rep.leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, Rep.FiniteCyclicGroup.resolution_complex, groupHomology.chainsFunctor_map, Rep.indCoindIso_inv_hom_toLinearMap, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, Rep.forget₂_moduleCat_map, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, groupHomology.map_id_comp_H0Iso_hom_apply, Rep.resCoindHomEquiv_apply, groupHomology.H1CoresCoinfOfTrivial_f, Rep.coindFunctor'_obj, Rep.instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype, groupHomology.functor_map, Rep.linearization_obj_V, groupHomology.mapCycles₂_id_comp_apply, Rep.mkIso_hom_hom, Rep.standardComplex.instQuasiIsoNatεToSingle₀, Rep.standardComplex.x_projective, Rep.instIsLeftAdjointResFunctor, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, Rep.FiniteCyclicGroup.resolution_quasiIso, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.η_def, Rep.sum_hom, groupCohomology.H1Map_id, Rep.hom_inv_leftUnitor, Rep.indFunctor_map, Rep.standardComplex.d_apply, groupHomology.H1CoresCoinfOfTrivial_g, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.π_comp_H0Iso_hom, Rep.hom_inv_associator, groupCohomology.mapShortComplexH1_id_comp_assoc, Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap, groupCohomology.mapShortComplexH1_zero, Rep.homEquiv_symm_apply, groupCohomology.mapShortComplexH1_comp_assoc, Rep.coinvariantsTensorMk_apply, groupHomology.H0π_comp_H0Iso_hom, Rep.add_comp, Rep.coinvariantsShortComplex_X₁, Rep.ihom_map, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, Rep.invariantsFunctor_map_hom, groupHomology.map_id_comp_H0Iso_hom, Rep.id_apply, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.cocyclesMap_id, Rep.invariantsAdjunction_counit_app, Rep.instHasBinaryBiproducts, Rep.norm_comm_assoc, groupCohomology.mapShortComplexH2_id_comp, Rep.resIndAdjunction_unit_app, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.ihom_coev_app_hom, Rep.leftRegular_projective, Rep.tensorUnit_V, groupHomology.chainsMap_zero, groupHomology.isIso_δ_of_isZero, groupHomology.mapShortComplexH2_id_comp, Rep.comp_smul, Rep.ofHom_sum, Rep.comp_apply, Rep.hom_tensorHom, Rep.indResHomEquiv_symm_apply, Rep.hom_comp, groupCohomology.map_cochainsFunctor_shortExact, groupCohomology.cocyclesMap_id_comp, Rep.hom_whiskerLeft, groupHomology.shortComplexH0_g, Rep.RepToAction_obj, groupCohomology.mapShortComplexH2_id, Rep.comp_add, Rep.instIsEquivalenceActionModuleCatActionToRep, groupHomology.inhomogeneousChains.d_eq, Rep.epi_iff_surjective, groupCohomology.cochainsFunctor_map, groupHomology.d₁₀_comp_coinvariantsMk_assoc, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Rep.coinvariantsShortComplex_X₂, groupHomology.H0π_comp_H0Iso_hom_assoc, Rep.ofHom_zsmul, groupHomology.cyclesMap_comp, Rep.ofHom_id, Rep.tensor_V, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, Rep.tensorHomEquiv_symm_apply, Rep.hom_inv_apply, Rep.tensorUnit_ρ, Rep.instMonoidalLinear, Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, Rep.coinvariantsAdjunction_homEquiv_apply_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomology.H1CoresCoinf_f, Rep.ihom_obj_ρ, groupCohomology.cochainsMap_id_comp_assoc, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, Rep.instIsLeftAdjointIndFunctor, Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, groupHomology.cyclesMap_id, Rep.instFaithfulResFunctor, Rep.instAdditiveModuleCatInvariantsFunctor, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Rep.ofHom_apply, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, Rep.coindFunctor'_map, Rep.coinvariantsFunctor_map_hom, Rep.coindFunctor_obj, groupCohomology.map_id_comp_H0Iso_hom_assoc, Rep.ihom_obj_ρ_def, Rep.coinvariantsShortComplex_X₃, Rep.reflectsIsomorphisms_forget, groupHomology.H0π_comp_H0Iso_hom_apply, Rep.mono_iff_injective, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.functor_map, Rep.mkIso_hom_hom_toLinearMap, Rep.Tor_obj, groupCohomology.mono_δ_of_isZero, Rep.coinvariantsShortComplex_shortExact, Rep.FiniteCyclicGroup.resolution_π, Rep.ofHom_zero, groupHomology.mapCycles₁_quotientGroupMk'_epi, Rep.instHasZeroObject, Rep.FiniteCyclicGroup.resolution.π_f, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Rep.instAdditiveModuleCatCoinvariantsFunctor, groupCohomology.cochainsFunctor_obj, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, Rep.ofHom_smul, Rep.ofHom_neg, groupCohomology.isIso_δ_of_isZero, Rep.norm_comm, groupHomology.δ₁_apply, Rep.neg_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, Rep.quotientToCoinvariantsFunctor_obj_V, groupCohomology.map_comp_assoc, groupCohomology.cochainsMap_id, Rep.instInjective, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun

---

← Back to Index