Rep

📁 Source: Mathlib/RepresentationTheory/Rep.lean

Statistics

Metric	Count
Definitions Rep, Rep, IsTrivial, linearHomEquiv, linearHomEquivComm, applyAsHom, counitIso, counitIsoAddEquiv, diagonal, diagonalHomEquiv, diagonalOneIsoLeftRegular, diagonalSuccIsoFree, diagonalSuccIsoTensorTrivial, equivalenceModuleMonoidAlgebra, finsupp, finsuppTensorLeft, finsuppTensorRight, free, freeLift, freeLiftLEquiv, homEquiv, ihom, instAddCommGroupCarrierVModuleCat, instCoeSortType, instModuleCarrierVModuleCat, instMonoidalActionTypeLinearization, instMonoidalClosed, leftRegular, leftRegularHom, leftRegularHomEquiv, leftRegularTensorTrivialIsoFree, linearization, linearizationOfMulActionIso, linearizationTrivialIso, mkQ, norm, normNatTrans, of, ofAlgebraAut, ofAlgebraAutOnUnits, ofDistribMulAction, ofModuleMonoidAlgebra, ofMulAction, ofMulActionSubsingletonIsoTrivial, ofMulDistribMulAction, ofQuotient, quotient, resOfQuotientIso, subrepresentation, subtype, toModuleMonoidAlgebra, toModuleMonoidAlgebraMap, trivial, trivialFunctor, unitIso, unitIsoAddEquiv, ρ, repOfTprodIso, instLinearRep	59
Theorems Action_ρ_eq_ρ, linearHomEquivComm_hom, linearHomEquivComm_symm_hom, linearHomEquiv_hom, linearHomEquiv_symm_hom, applyAsHom_comm, applyAsHom_comm_apply, applyAsHom_comm_assoc, applyAsHom_hom, coe_linearization_obj, coe_linearization_obj_ρ, coe_of, coe_res_obj_ρ, diagonalHomEquiv_apply, diagonalHomEquiv_symm_apply, diagonalOneIsoLeftRegular_hom_hom, diagonalOneIsoLeftRegular_inv_hom, diagonalSuccIsoFree_hom_hom_single, diagonalSuccIsoFree_inv_hom_single, diagonalSuccIsoFree_inv_hom_single_single, diagonalSuccIsoTensorTrivial_hom_hom_single, diagonalSuccIsoTensorTrivial_inv_hom_single_left, diagonalSuccIsoTensorTrivial_inv_hom_single_right, diagonalSuccIsoTensorTrivial_inv_hom_single_single, diagonal_succ_projective, epi_iff_surjective, finsuppTensorLeft_hom_hom, finsuppTensorLeft_inv_hom, finsuppTensorRight_hom_hom, finsuppTensorRight_inv_hom, freeLiftLEquiv_apply, freeLiftLEquiv_symm_apply, freeLift_hom, freeLift_hom_single_single, free_ext, free_ext_iff, free_projective, homEquiv_apply_hom, homEquiv_def, homEquiv_symm_apply_hom, hom_comm_apply, ihom_coev_app_hom, ihom_ev_app_hom, ihom_map_hom, ihom_obj_V_carrier, ihom_obj_V_isAddCommGroup, ihom_obj_V_isModule, ihom_obj_ρ, ihom_obj_ρ_apply, ihom_obj_ρ_def, instEnoughProjectives, instEpiModuleCatHom, instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ, instIsTrivialObjModuleCatTrivialFunctor, instIsTrivialOfOfIsTrivial, instIsTrivialTrivial, instMonoModuleCatHom, instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, leftRegularHomEquiv_apply, leftRegularHomEquiv_symm_apply, leftRegularHomEquiv_symm_single, leftRegularHom_hom, leftRegularHom_hom_single, leftRegularTensorTrivialIsoFree_hom_hom, leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, leftRegularTensorTrivialIsoFree_inv_hom, leftRegularTensorTrivialIsoFree_inv_hom_single_single, leftRegular_projective, linearizationTrivialIso_hom_hom, linearizationTrivialIso_inv_hom, linearization_map_hom, linearization_map_hom_single, linearization_obj_ρ, linearization_single, linearization_δ_hom, linearization_ε_hom, linearization_η_hom_apply, linearization_μ_hom, mkQ_hom, mono_iff_injective, normNatTrans_app, norm_comm, norm_comm_apply, norm_comm_assoc, norm_hom, ofDistribMulAction_ρ_apply_apply, ofHom_ρ, ofModuleMonoidAlgebra_obj_coe, ofModuleMonoidAlgebra_obj_ρ, ofMulActionSubsingletonIsoTrivial_hom_hom, ofMulActionSubsingletonIsoTrivial_inv_hom, ofMulDistribMulAction_ρ_apply_apply, of_ρ, res_obj_ρ, subtype_hom, tensor_ρ, toAdditive_apply, toAdditive_symm_apply, to_Module_monoidAlgebra_map_aux, trivialFunctor_map_hom, trivialFunctor_obj_V, trivial_def, trivial_projective_of_subsingleton, unit_iso_comm, ρ_hom, repOfTprodIso_apply, repOfTprodIso_inv_apply	108
Total	167

GromovHausdorff.GHSpace

Definitions

Name	Category	Theorems
Rep 📖	CompOp	4 math math: GromovHausdorff.dist_ghDist, GromovHausdorff.rep_gHSpace_compactSpace, GromovHausdorff.rep_gHSpace_nonempty, toGHSpace_rep

Rep

Definitions

Name	Category	Theorems
IsTrivial 📖	MathDef	3 math math: instIsTrivialObjModuleCatTrivialFunctor, instIsTrivialTrivial, instIsTrivialOfOfIsTrivial
applyAsHom 📖	CompOp	18 math math: FiniteCyclicGroup.chainComplexFunctor_obj, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, applyAsHom_comm_apply, 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_hom, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff
counitIso 📖	CompOp	—
counitIsoAddEquiv 📖	CompOp	—
diagonal 📖	CompOp	13 math math: diagonalSuccIsoFree_inv_hom_single, diagonalSuccIsoTensorTrivial_inv_hom_single_left, diagonalHomEquiv_symm_apply, diagonalSuccIsoTensorTrivial_inv_hom_single_right, diagonalSuccIsoTensorTrivial_inv_hom_single_single, diagonalSuccIsoFree_inv_hom_single_single, diagonal_succ_projective, diagonalOneIsoLeftRegular_inv_hom, diagonalSuccIsoTensorTrivial_hom_hom_single, diagonalOneIsoLeftRegular_hom_hom, diagonalHomEquiv_apply, diagonalSuccIsoFree_hom_hom_single, barComplex.d_comp_diagonalSuccIsoFree_inv_eq
diagonalHomEquiv 📖	CompOp	2 math math: diagonalHomEquiv_symm_apply, diagonalHomEquiv_apply
diagonalOneIsoLeftRegular 📖	CompOp	2 math math: diagonalOneIsoLeftRegular_inv_hom, diagonalOneIsoLeftRegular_hom_hom
diagonalSuccIsoFree 📖	CompOp	4 math math: diagonalSuccIsoFree_inv_hom_single, diagonalSuccIsoFree_inv_hom_single_single, diagonalSuccIsoFree_hom_hom_single, barComplex.d_comp_diagonalSuccIsoFree_inv_eq
diagonalSuccIsoTensorTrivial 📖	CompOp	4 math math: diagonalSuccIsoTensorTrivial_inv_hom_single_left, diagonalSuccIsoTensorTrivial_inv_hom_single_right, diagonalSuccIsoTensorTrivial_inv_hom_single_single, diagonalSuccIsoTensorTrivial_hom_hom_single
equivalenceModuleMonoidAlgebra 📖	CompOp	—
finsupp 📖	CompOp	4 math math: finsuppTensorRight_hom_hom, finsuppTensorRight_inv_hom, finsuppTensorLeft_inv_hom, finsuppTensorLeft_hom_hom
finsuppTensorLeft 📖	CompOp	2 math math: finsuppTensorLeft_inv_hom, finsuppTensorLeft_hom_hom
finsuppTensorRight 📖	CompOp	2 math math: finsuppTensorRight_hom_hom, finsuppTensorRight_inv_hom
free 📖	CompOp	19 math math: diagonalSuccIsoFree_inv_hom_single, coinvariantsTensorFreeLEquiv_symm_apply, free_projective, diagonalSuccIsoFree_inv_hom_single_single, coinvariantsTensorFreeLEquiv_apply, freeLiftLEquiv_apply, inhomogeneousCochains.d_eq, leftRegularTensorTrivialIsoFree_inv_hom, freeLift_hom, freeLift_hom_single_single, leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, freeLiftLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, diagonalSuccIsoFree_hom_hom_single, free_ext_iff, barComplex.d_comp_diagonalSuccIsoFree_inv_eq, leftRegularTensorTrivialIsoFree_hom_hom, barComplex.d_single, leftRegularTensorTrivialIsoFree_inv_hom_single_single
freeLift 📖	CompOp	3 math math: freeLift_hom, freeLift_hom_single_single, freeLiftLEquiv_symm_apply
freeLiftLEquiv 📖	CompOp	3 math math: freeLiftLEquiv_apply, inhomogeneousCochains.d_eq, freeLiftLEquiv_symm_apply
homEquiv 📖	CompOp	3 math math: homEquiv_apply_hom, homEquiv_def, homEquiv_symm_apply_hom
ihom 📖	CompOp	9 math math: homEquiv_apply_hom, ihom_obj_ρ_apply, ihom_obj_V_isAddCommGroup, ihom_map_hom, homEquiv_symm_apply_hom, ihom_obj_V_isModule, ihom_obj_ρ, ihom_obj_ρ_def, ihom_obj_V_carrier
instAddCommGroupCarrierVModuleCat 📖	CompOp	422 math math: resCoindHomEquiv_symm_apply_hom, resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, groupHomology.π_comp_H2Iso_hom_assoc, invariantsAdjunction_homEquiv_symm_apply_hom, groupHomology.mapCycles₂_comp_assoc, 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₂, groupCohomology.d₀₁_comp_d₁₂, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, groupCohomology.cocyclesIso₀_hom_comp_f, resCoindAdjunction_counit_app_hom_hom, groupHomology.d₃₂_single, groupCohomology.eq_d₀₁_comp_inv, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, leftRegularHom_hom, groupCohomology.π_comp_H0Iso_hom, groupCohomology.π_comp_H1Iso_hom_assoc, groupCohomology.eq_d₁₂_comp_inv, indToCoindAux_self, groupCohomology.mapCocycles₂_comp_i, groupHomology.eq_d₃₂_comp_inv, coe_res_obj_ρ, diagonalHomEquiv_symm_apply, groupCohomology.H0IsoOfIsTrivial_hom, groupCohomology.coe_mapCocycles₁, groupHomology.mem_cycles₂_iff, 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, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, groupCohomology.comp_d₁₂_eq, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, linearization_single, groupHomology.d₃₂_single_one_thd, 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, groupCohomology.eq_d₁₂_comp_inv_apply, groupHomology.chains₁ToCoinvariantsKer_surjective, coinvariantsTensorFreeLEquiv_symm_apply, groupHomology.cycles₁_eq_top_of_isTrivial, resCoindAdjunction_unit_app_hom_hom, groupHomology.d₃₂_comp_d₂₁_assoc, groupCohomology.mem_cocycles₁_def, homEquiv_apply_hom, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, coindFunctorIso_hom_app_hom_hom_apply_hom_hom_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, 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, ρ_hom, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.eq_d₂₁_comp_inv, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, ihom_ev_app_hom, groupCohomology.dArrowIso₀₁_hom_right, groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, groupHomology.mapCycles₁_comp_i, groupCohomology.shortComplexH0_f, groupCohomology.cocyclesOfIsCocycle₁_coe, groupCohomology.coboundaries₂_le_cocycles₂, coindVEquiv_symm_apply_coe, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, groupCohomology.comp_d₂₃_eq, groupCohomology.coboundaries₂.val_eq_coe, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupCohomology.infNatTrans_app, groupCohomology.d₁₂_apply_mem_cocycles₂, invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, groupCohomology.d₀₁_apply_mem_cocycles₁, indToCoindAux_fst_mul_inv, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupHomology.chainsMap_f_single, groupCohomology.subtype_comp_d₀₁_apply, groupCohomology.H2π_eq_iff, groupCohomology.comp_d₀₁_eq, groupCohomology.cocycles₂_map_one_snd, coinvariantsTensorFreeLEquiv_apply, groupHomology.toCycles_comp_isoCycles₁_hom_apply, groupHomology.mapCycles₂_comp_i, groupCohomology.map_H0Iso_hom_f, groupHomology.boundariesOfIsBoundary₁_coe, indToCoindAux_comm, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, groupHomology.eq_d₃₂_comp_inv_apply, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, toAdditive_symm_apply, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, ofMulDistribMulAction_ρ_apply_apply, instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ, groupCohomology.instEpiModuleCatH1π, groupCohomology.H2π_comp_map, groupHomology.π_comp_H2Iso_hom, indResAdjunction_counit_app_hom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, groupCohomology.isoCocycles₂_hom_comp_i, groupCohomology.π_comp_H0Iso_hom_apply, groupHomology.coe_mapCycles₂, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, groupHomology.H1π_comp_map_apply, groupCohomology.dArrowIso₀₁_hom_left, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, groupCohomology.eq_d₀₁_comp_inv_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, freeLiftLEquiv_apply, groupCohomology.mapCocycles₁_one, groupHomology.H2π_comp_map_assoc, indToCoindAux_mul_fst, ihom_obj_ρ_apply, groupHomology.d₁₀ArrowIso_inv_right, finsuppTensorRight_hom_hom, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, groupCohomology.mem_cocycles₂_iff, tensor_ρ, toAdditive_apply, groupCohomology.H2π_comp_map_assoc, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.d₂₁_comp_d₁₀_apply, groupHomology.mapCycles₂_comp_apply, coindFunctorIso_inv_app_hom_hom_apply_coe, ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, leftRegularHomEquiv_symm_apply, groupHomology.H2π_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, groupCohomology.inhomogeneousCochains.d_comp_d, groupHomology.isoCycles₂_hom_comp_i_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, groupHomology.eq_d₂₁_comp_inv_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, groupHomology.inhomogeneousChains.d_single, groupCohomology.coboundariesOfIsCoboundary₁_coe, Representation.coind'_apply_apply, groupCohomology.d₁₂_comp_d₂₃_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, coindIso_inv_hom_hom, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, groupCohomology.subtype_comp_d₀₁_assoc, 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, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupHomology.eq_d₁₀_comp_inv, groupHomology.isoShortComplexH1_inv, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, groupHomology.eq_d₁₀_comp_inv_assoc, groupCohomology.d₁₂_comp_d₂₃, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, linearization_obj_ρ, toCoinvariantsMkQ_hom, 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, groupCohomology.H1π_eq_zero_iff, groupHomology.H1AddEquivOfIsTrivial_symm_apply, invariantsAdjunction_counit_app_hom, groupCohomology.cochainsMap_f, groupCohomology.coboundaries₁.val_eq_coe, groupHomology.d₃₂_single_one_fst, inhomogeneousCochains.d_hom_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, groupHomology.d₂₁_comp_d₁₀, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, 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, groupHomology.cyclesOfIsCycle₁_coe, quotientToInvariantsFunctor_obj_V, groupHomology.inhomogeneousChains.ext_iff, 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, groupCohomology.cocycles₁.val_eq_coe, groupCohomology.H1π_comp_map_apply, leftRegularHom_hom_single, groupCohomology.cocycles₁_map_one, groupHomology.eq_d₃₂_comp_inv_assoc, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, finsuppTensorRight_inv_hom, ihom_obj_V_isAddCommGroup, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, coindVEquiv_apply_hom, 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.H2π_comp_map, groupCohomology.cocycles₂.val_eq_coe, groupCohomology.eq_d₂₃_comp_inv, FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.H1π_comp_map_assoc, ihom_map_hom, groupHomology.instEpiModuleCatH1π, groupHomology.H1AddEquivOfIsTrivial_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles, coinvariantsTensor_hom_ext_iff, finsuppTensorLeft_inv_hom, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, unit_iso_comm, leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, groupHomology.instEpiModuleCatH2π, groupCohomology.cocyclesMk₂_eq, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, groupHomology.d₃₂_apply_mem_cycles₂, ofHom_ρ, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, groupHomology.boundariesOfIsBoundary₂_coe, groupHomology.cyclesMk₁_eq, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, groupCohomology.mapCocycles₁_comp_i_apply, coindMap_hom, groupHomology.mapCycles₂_id_comp_apply, trivial_def, groupCohomology.cocycles₂_ext_iff, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, invariantsAdjunction_homEquiv_apply_hom, hom_comm_apply, groupHomology.H2π_comp_map_apply, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, groupCohomology.cochainsMap_f_hom, groupCohomology.coboundaries₁_ext_iff, finsuppTensorLeft_hom_hom, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.inhomogeneousChains.d_comp_d, groupCohomology.π_comp_H2Iso_hom_apply, coinvariantsTensorMk_apply, groupHomology.isoCycles₁_hom_comp_i_assoc, homEquiv_symm_apply_hom, invariantsFunctor_map_hom, groupHomology.d₁₀_eq_zero_of_isTrivial, groupCohomology.π_comp_H1Iso_hom_apply, groupCohomology.d₀₁_comp_d₁₂_assoc, groupHomology.d₂₁_single_one_snd, 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, leftRegularHomEquiv_apply, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, 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, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupHomology.boundariesToCycles₂_apply, groupCohomology.subtype_comp_d₀₁, groupHomology.cyclesOfIsCycle₂_coe, freeLift_hom, 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, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, res_obj_ρ, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, groupCohomology.coboundaries₁_le_cocycles₁, ihom_obj_V_isModule, groupHomology.d₁₀ArrowIso_hom_right, freeLift_hom_single_single, groupHomology.single_one_mem_boundaries₁, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, groupCohomology.isoCocycles₂_hom_comp_i_apply, diagonalHomEquiv_apply, groupHomology.d₂₁_single, freeLiftLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, groupHomology.eq_d₂₁_comp_inv_apply, groupCohomology.coboundaries₂_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MonoidalClosed.linearHomEquivComm_symm_hom, indToCoindAux_of_not_rel, groupCohomology.cocyclesOfIsCocycle₂_coe, groupHomology.isoCycles₁_hom_comp_i, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, applyAsHom_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupCohomology.H1π_comp_map, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, groupCohomology.cocyclesMk₀_eq, groupHomology.lsingle_comp_chainsMap_f_assoc, groupHomology.single_mem_cycles₂_iff, groupCohomology.isoShortComplexH1_inv, groupHomology.boundaries₁_le_cycles₁, ihom_obj_ρ, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, groupCohomology.cocycles₁_ext_iff, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, groupCohomology.eq_d₁₂_comp_inv_assoc, Representation.linHom.invariantsEquivRepHom_apply_hom, groupCohomology.H1InfRes_f, groupHomology.d₁₀ArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, groupHomology.single_mem_cycles₁_iff, 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, ihom_obj_V_carrier, coindIso_hom_hom_hom, groupHomology.d₂₁_comp_d₁₀_assoc, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, groupCohomology.isoCocycles₁_hom_comp_i_assoc, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.mapCycles₁_comp_i_assoc, coinvariantsTensorFreeToFinsupp_mk_tmul_single, groupCohomology.coboundariesOfIsCoboundary₂_coe, groupHomology.mem_cycles₁_iff, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, groupCohomology.cocycles₁.d₁₂_apply, indResHomEquiv_symm_apply_hom, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, groupCohomology.π_comp_H2Iso_hom, groupHomology.H2π_eq_zero_iff, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, groupHomology.H1π_eq_iff, groupHomology.d₃₂_comp_d₂₁_apply, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom, groupCohomology.d₀₁_eq_zero
instCoeSortType 📖	CompOp	—
instModuleCarrierVModuleCat 📖	CompOp	—
instMonoidalActionTypeLinearization 📖	CompOp	4 math math: linearization_η_hom_apply, linearization_δ_hom, linearization_ε_hom, linearization_μ_hom
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
leftRegular 📖	CompOp	33 math math: leftRegularHom_hom, diagonalSuccIsoTensorTrivial_inv_hom_single_left, diagonalSuccIsoTensorTrivial_inv_hom_single_right, diagonalSuccIsoTensorTrivial_inv_hom_single_single, coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coindVEquiv_symm_apply_coe, coindMap'_hom, coindFunctorIso_inv_app_hom_hom_apply_coe, leftRegularHomEquiv_symm_apply, Representation.coind'_apply_apply, diagonalOneIsoLeftRegular_inv_hom, coindIso_inv_hom_hom, diagonalSuccIsoTensorTrivial_hom_hom_single, coind'_ext_iff, leftRegularHom_hom_single, coindVEquiv_apply_hom, leftRegularHomEquiv_symm_single, FiniteCyclicGroup.resolution_complex, leftRegularTensorTrivialIsoFree_inv_hom, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, FiniteCyclicGroup.resolution_quasiIso, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, diagonalOneIsoLeftRegular_hom_hom, leftRegularHomEquiv_apply, leftRegular_projective, leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, coindIso_hom_hom_hom, leftRegularTensorTrivialIsoFree_hom_hom, FiniteCyclicGroup.resolution.π_f, FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, leftRegularTensorTrivialIsoFree_inv_hom_single_single
leftRegularHom 📖	CompOp	4 math math: leftRegularHom_hom, leftRegularHomEquiv_symm_apply, leftRegularHom_hom_single, FiniteCyclicGroup.resolution.π_f
leftRegularHomEquiv 📖	CompOp	4 math math: leftRegularHomEquiv_symm_apply, Representation.coind'_apply_apply, leftRegularHomEquiv_symm_single, leftRegularHomEquiv_apply
leftRegularTensorTrivialIsoFree 📖	CompOp	4 math math: leftRegularTensorTrivialIsoFree_inv_hom, leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, leftRegularTensorTrivialIsoFree_hom_hom, leftRegularTensorTrivialIsoFree_inv_hom_single_single
linearization 📖	CompOp	12 math math: coe_linearization_obj_ρ, linearization_single, coe_linearization_obj, linearization_η_hom_apply, linearization_obj_ρ, linearizationTrivialIso_inv_hom, linearization_δ_hom, linearizationTrivialIso_hom_hom, linearization_map_hom_single, linearization_ε_hom, linearization_map_hom, linearization_μ_hom
linearizationOfMulActionIso 📖	CompOp	—
linearizationTrivialIso 📖	CompOp	2 math math: linearizationTrivialIso_inv_hom, linearizationTrivialIso_hom_hom
mkQ 📖	CompOp	2 math math: groupHomology.coinfNatTrans_app, mkQ_hom
norm 📖	CompOp	15 math math: FiniteCyclicGroup.chainComplexFunctor_obj, norm_comm_apply, 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_hom, 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	7 math math: Representation.repOfTprodIso_inv_apply, Representation.repOfTprodIso_apply, instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ, coe_of, of_ρ, ihom_map_hom, instIsTrivialOfOfIsTrivial
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
ofModuleMonoidAlgebra 📖	CompOp	3 math math: ofModuleMonoidAlgebra_obj_coe, ofModuleMonoidAlgebra_obj_ρ, unit_iso_comm
ofMulAction 📖	CompOp	3 math math: ofMulActionSubsingletonIsoTrivial_inv_hom, ofMulActionSubsingletonIsoTrivial_hom_hom, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq
ofMulActionSubsingletonIsoTrivial 📖	CompOp	2 math math: ofMulActionSubsingletonIsoTrivial_inv_hom, ofMulActionSubsingletonIsoTrivial_hom_hom
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
ofQuotient 📖	CompOp	4 math math: groupHomology.map₁_quotientGroupMk'_epi, groupHomology.H1CoresCoinfOfTrivial_g, groupHomology.H1CoresCoinfOfTrivial_X₃, groupHomology.mapCycles₁_quotientGroupMk'_epi
quotient 📖	CompOp	1 math math: mkQ_hom
resOfQuotientIso 📖	CompOp	3 math math: groupHomology.map₁_quotientGroupMk'_epi, groupHomology.H1CoresCoinfOfTrivial_g, groupHomology.mapCycles₁_quotientGroupMk'_epi
subrepresentation 📖	CompOp	1 math math: subtype_hom
subtype 📖	CompOp	4 math math: subtype_hom, groupCohomology.infNatTrans_app, coinvariantsShortComplex_f, groupCohomology.H1InfRes_f
toModuleMonoidAlgebra 📖	CompOp	1 math math: unit_iso_comm
toModuleMonoidAlgebraMap 📖	CompOp	—
trivial 📖	CompOp	31 math math: diagonalSuccIsoTensorTrivial_inv_hom_single_left, coinvariantsAdjunction_counit_app, diagonalSuccIsoTensorTrivial_inv_hom_single_right, diagonalSuccIsoTensorTrivial_inv_hom_single_single, trivial_projective_of_subsingleton, instIsTrivialTrivial, standardComplex.εToSingle₀_comp_eq, barResolution_complex, ofMulActionSubsingletonIsoTrivial_inv_hom, diagonalSuccIsoTensorTrivial_hom_hom_single, ofMulActionSubsingletonIsoTrivial_hom_hom, linearizationTrivialIso_inv_hom, standardComplex.quasiIso_forget₂_εToSingle₀, standardComplex.d_comp_ε, trivialFunctor_map_hom, FiniteCyclicGroup.resolution_complex, leftRegularTensorTrivialIsoFree_inv_hom, standardComplex.instQuasiIsoNatεToSingle₀, trivial_def, FiniteCyclicGroup.resolution_quasiIso, FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, linearizationTrivialIso_hom_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, leftRegularTensorTrivialIsoFree_hom_hom, FiniteCyclicGroup.resolution_π, FiniteCyclicGroup.resolution.π_f, leftRegularTensorTrivialIsoFree_inv_hom_single_single, 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, invariantsAdjunction_counit_app_hom, trivialFunctor_map_hom, invariantsAdjunction_homEquiv_apply_hom, coinvariantsAdjunction_unit_app_hom, coinvariantsAdjunction_homEquiv_apply_hom
unitIso 📖	CompOp	—
unitIsoAddEquiv 📖	CompOp	1 math math: unit_iso_comm
ρ 📖	CompOp	149 math math: resCoindHomEquiv_symm_apply_hom, resCoindHomEquiv_apply_hom, invariantsAdjunction_homEquiv_symm_apply_hom, coe_linearization_obj_ρ, groupCohomology.mem_cocycles₂_def, groupHomology.coinfNatTrans_app, groupCohomology.d₂₃_hom_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, groupCohomology.cocyclesIso₀_hom_comp_f, resCoindAdjunction_counit_app_hom_hom, groupHomology.d₃₂_single, leftRegularHom_hom, groupCohomology.π_comp_H0Iso_hom, coe_res_obj_ρ, diagonalHomEquiv_symm_apply, groupCohomology.H0IsoOfIsTrivial_hom, groupHomology.mem_cycles₂_iff, groupCohomology.d₁₂_hom_apply, groupCohomology.d₀₁_hom_apply, linearization_single, groupHomology.d₃₂_single_one_thd, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, finsuppToCoinvariantsTensorFree_single, groupHomology.chains₁ToCoinvariantsKer_surjective, coinvariantsTensorFreeLEquiv_symm_apply, resCoindAdjunction_unit_app_hom_hom, groupCohomology.mem_cocycles₁_def, FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupHomology.d₂₁_single_inv_mul_ρ_add_single, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupHomology.d₁₀_comp_coinvariantsMk_apply, ρ_hom, groupCohomology.shortComplexH0_f, coindVEquiv_symm_apply_coe, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, groupCohomology.infNatTrans_app, invariantsAdjunction_unit_app, coinvariantsFunctor_obj_carrier, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupCohomology.subtype_comp_d₀₁_apply, groupCohomology.cocycles₂_map_one_snd, coinvariantsTensorFreeLEquiv_apply, groupCohomology.map_H0Iso_hom_f, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, ofMulDistribMulAction_ρ_apply_apply, instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ, indResAdjunction_counit_app_hom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, coindToInd_apply, FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupCohomology.π_comp_H0Iso_hom_apply, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, indToCoindAux_mul_fst, ihom_obj_ρ_apply, groupCohomology.π_comp_H0Iso_hom_assoc, groupCohomology.mem_cocycles₂_iff, tensor_ρ, coindFunctorIso_inv_app_hom_hom_apply_coe, ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, ofModuleMonoidAlgebra_obj_ρ, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, coinvariantsShortComplex_f, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupHomology.inhomogeneousChains.d_single, coindIso_inv_hom_hom, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.subtype_comp_d₀₁_assoc, groupCohomology.map_id_comp_H0Iso_hom, indToCoindAux_mul_snd, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, linearization_obj_ρ, toCoinvariantsMkQ_hom, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, of_ρ, invariantsAdjunction_counit_app_hom, inhomogeneousCochains.d_hom_apply, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, quotientToInvariantsFunctor_obj_V, leftRegularHom_hom_single, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, coinvariantsMk_app_hom, coindVEquiv_apply_hom, ihom_map_hom, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, unit_iso_comm, leftRegularHomEquiv_symm_single, norm_hom, indResAdjunction_unit_app_hom_hom, ofHom_ρ, groupHomology.map_id_comp_H0Iso_hom_apply, Action_ρ_eq_ρ, coindMap_hom, trivial_def, invariantsAdjunction_homEquiv_apply_hom, hom_comm_apply, FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, FiniteCyclicGroup.groupHomologyπOdd_eq_iff, coinvariantsTensorMk_apply, indMap_hom, FDRep.forget₂_ρ, invariantsFunctor_map_hom, groupHomology.d₂₁_single_one_snd, groupHomology.d₃₂_single_one_snd, coinvariantsTensorIndHom_mk_tmul_indVMk, Representation.linHom.mem_invariants_iff_comm, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupCohomology.subtype_comp_d₀₁, freeLift_hom, groupHomology.d₁₀_single_inv, res_obj_ρ, freeLift_hom_single_single, groupHomology.d₂₁_single, groupHomology.inhomogeneousChains.d_eq, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, applyAsHom_hom, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, indResHomEquiv_apply_hom, groupCohomology.cocyclesMk₀_eq, groupHomology.single_mem_cycles₂_iff, FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, ihom_obj_ρ, groupCohomology.map_H0Iso_hom_f_assoc, coinvariantsTensorIndInv_mk_tmul_indMk, Representation.linHom.invariantsEquivRepHom_apply_hom, groupCohomology.H1InfRes_f, 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, coindIso_hom_hom_hom, groupHomology.H0π_comp_H0Iso_hom_apply, coinvariantsTensorFreeToFinsupp_mk_tmul_single, groupHomology.mem_cycles₁_iff, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, indResHomEquiv_symm_apply_hom, FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Action_ρ_eq_ρ 📖	mathematical	—	Action.ρ ModuleCat CommRing.toRing ModuleCat.moduleCategory MonoidHom.comp LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V 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 ρ	—	—
applyAsHom_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CommMonoid.toMonoid CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory applyAsHom	—	Action.hom_ext ModuleCat.hom_ext LinearMap.ext hom_comm_apply
applyAsHom_comm_apply 📖	mathematical	—	DFunLike.coe Action.HomSubtype ModuleCat CommRing.toRing ModuleCat.moduleCategory CommMonoid.toMonoid LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CategoryTheory.ConcreteCategory.hom Rep Action.instCategory Action.instConcreteCategoryHomSubtypeV applyAsHom	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise applyAsHom_comm
applyAsHom_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CommMonoid.toMonoid CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory applyAsHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' applyAsHom_comm
applyAsHom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CommMonoid.toMonoid applyAsHom ModuleCat.ofHom ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule DFunLike.coe Representation Action.V CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
coe_linearization_obj 📖	mathematical	—	ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
coe_linearization_obj_ρ 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Action.V CategoryTheory.types MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike ρ CategoryTheory.Functor.obj Action Action.instCategory Rep CommRing.toRing ModuleCat ModuleCat.moduleCategory linearization Finsupp.lmapDomain CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.monoid Action.ρ	—	—
coe_of 📖	mathematical	—	ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory of	—	—
coe_res_obj_ρ 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike ρ CategoryTheory.Functor.obj Action Action.instCategory Action.res Representation	—	—
diagonalHomEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory diagonal AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Pi.addCommMonoid ModuleCat.carrier Action.V instAddCommGroupCarrierVModuleCat CategoryTheory.Linear.homModule instLinearRep Pi.Function.module ModuleCat.isModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv diagonalHomEquiv CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Fin.partialProd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids CategoryTheory.Category.comp_id diagonalSuccIsoFree_inv_hom_single_single one_smul
diagonalHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid diagonal ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Pi.addCommMonoid instAddCommGroupCarrierVModuleCat CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Pi.Function.module CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm diagonalHomEquiv Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomInvPair.ids RingHomCompTriple.ids CategoryTheory.Category.comp_id diagonalSuccIsoFree_hom_hom_single Finsupp.uncurry_single Finsupp.linearCombination_single one_smul
diagonalOneIsoLeftRegular_hom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory diagonal leftRegular CategoryTheory.Iso.hom Rep Action.instCategory diagonalOneIsoLeftRegular ModuleCat.ofHom Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearEquiv.toLinearMap Ring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid Finsupp.domLCongr NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Equiv.funUnique Fin.instUnique	—	—
diagonalOneIsoLeftRegular_inv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory leftRegular diagonal CategoryTheory.Iso.inv Rep Action.instCategory diagonalOneIsoLeftRegular ModuleCat.ofHom Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearEquiv.toLinearMap Ring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid Finsupp.domLCongr NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Equiv.symm Equiv.funUnique Fin.instUnique	—	Finsupp.domLCongr_symm
diagonalSuccIsoFree_hom_hom_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid diagonal free ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.hom Rep Action.instCategory diagonalSuccIsoFree Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	diagonalSuccIsoTensorTrivial_hom_hom_single leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single one_mul
diagonalSuccIsoFree_inv_hom_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid free diagonal ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.inv Rep Action.instCategory diagonalSuccIsoFree Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule AddEquiv Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike Finsupp.lift Function.hasSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Fin.partialProd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Finsupp.induction Finsupp.single_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.smul_single mul_one Finsupp.single_add map_add SemilinearMapClass.toAddHomClass diagonalSuccIsoFree_inv_hom_single_single Finsupp.sum_add_index' Finsupp.sum_single_index
diagonalSuccIsoFree_inv_hom_single_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid free diagonal ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.inv Rep Action.instCategory diagonalSuccIsoFree Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero Function.hasSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Fin.partialProd	—	diagonalSuccIsoTensorTrivial_inv_hom_single_single leftRegularTensorTrivialIsoFree_inv_hom_single_single mul_one
diagonalSuccIsoTensorTrivial_hom_hom_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ModuleCat.carrier CommRing.toRing CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat ModuleCat.moduleCategory ModuleCat.MonoidalCategory.instMonoidalCategoryStruct ModuleCat.of Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid diagonal Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Action.Hom.hom CategoryTheory.Iso.hom diagonalSuccIsoTensorTrivial Finsupp.single TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomCompTriple.ids RingHomInvPair.ids CategoryTheory.MonoidalCategory.id_tensorHom ModuleCat.hom_id LinearMap.lTensor_id LinearMap.comp.congr_simp Finsupp.mapDomain_single Action.diagonalSuccIsoTensorTrivial_hom_hom_apply finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
diagonalSuccIsoTensorTrivial_inv_hom_single_left 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule diagonal ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.inv diagonalSuccIsoTensorTrivial TensorProduct.tmul CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence Finsupp.single NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid AddEquiv Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike Finsupp.lift Function.hasSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Fin.partialProd	—	Finsupp.induction TensorProduct.tmul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.tmul_add map_add SemilinearMapClass.toAddHomClass Finsupp.smul_single Finsupp.sum_single_index MulZeroClass.zero_mul Finsupp.single_zero mul_comm Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd diagonalSuccIsoTensorTrivial_inv_hom_single_single
diagonalSuccIsoTensorTrivial_inv_hom_single_right 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule diagonal ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.inv diagonalSuccIsoTensorTrivial TensorProduct.tmul CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence Finsupp.single NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid AddEquiv Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike Finsupp.lift Function.hasSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Fin.partialProd	—	Finsupp.induction TensorProduct.zero_tmul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.add_tmul map_add SemilinearMapClass.toAddHomClass Finsupp.smul_single Finsupp.sum_single_index MulZeroClass.zero_mul Finsupp.single_zero Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd diagonalSuccIsoTensorTrivial_inv_hom_single_single
diagonalSuccIsoTensorTrivial_inv_hom_single_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule diagonal ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.inv diagonalSuccIsoTensorTrivial TensorProduct.tmul CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence Finsupp.single NonAssocSemiring.toNonUnitalNonAssocSemiring Function.hasSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Fin.partialProd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Action.diagonalSuccIsoTensorTrivial_inv_hom_apply RingHomCompTriple.ids RingHomInvPair.ids CategoryTheory.Category.assoc ModuleCat.hom_id TensorProduct.map_id LinearMap.comp.congr_simp finsuppTensorFinsupp'_single_tmul_single Finsupp.mapDomain_single
diagonal_succ_projective 📖	mathematical	—	CategoryTheory.Projective Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory diagonal	—	CategoryTheory.Projective.of_iso free_projective
epi_iff_surjective 📖	mathematical	—	CategoryTheory.Epi Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory ModuleCat.carrier Action.V DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom	—	ModuleCat.epi_iff_surjective CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.forget₂_faithful
finsuppTensorLeft_hom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory finsupp CategoryTheory.Iso.hom finsuppTensorLeft ModuleCat.ofHom TensorProduct CommRing.toCommSemiring Finsupp ModuleCat.carrier Action.V AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring ModuleCat.isModule TensorProduct.zero TensorProduct.addCommGroup Finsupp.instAddCommGroup TensorProduct.leftModule Ring.toSemiring ModuleCat.isAddCommGroup TensorProduct.addCommMonoid LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.finsuppLeft Algebra.id	—	—
finsuppTensorLeft_inv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory finsupp CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.Iso.inv finsuppTensorLeft ModuleCat.ofHom Finsupp TensorProduct CommRing.toCommSemiring ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule TensorProduct.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring Finsupp.instAddCommGroup TensorProduct.addCommGroup ModuleCat.isAddCommGroup Ring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearEquiv.symm TensorProduct.finsuppLeft Algebra.id	—	—
finsuppTensorRight_hom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory finsupp CategoryTheory.Iso.hom finsuppTensorRight ModuleCat.ofHom TensorProduct CommRing.toCommSemiring ModuleCat.carrier Action.V Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Finsupp.instAddCommMonoid ModuleCat.isModule Finsupp.module CommSemiring.toSemiring TensorProduct.zero TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.leftModule Ring.toSemiring Finsupp.instAddCommGroup TensorProduct.addCommMonoid LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.finsuppRight Algebra.id	—	—
finsuppTensorRight_inv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory finsupp CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.Iso.inv finsuppTensorRight ModuleCat.ofHom Finsupp TensorProduct CommRing.toCommSemiring ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule TensorProduct.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring Finsupp.instAddCommGroup TensorProduct.addCommGroup ModuleCat.isAddCommGroup Ring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearEquiv.symm TensorProduct.finsuppRight Algebra.id	—	—
freeLiftLEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory free AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Pi.addCommMonoid ModuleCat.carrier Action.V instAddCommGroupCarrierVModuleCat CategoryTheory.Linear.homModule instLinearRep Pi.Function.module ModuleCat.isModule EquivLike.toFunLike LinearEquiv.instEquivLike freeLiftLEquiv CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids
freeLiftLEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory free Pi.addCommMonoid ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Pi.Function.module ModuleCat.isModule CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm freeLiftLEquiv freeLift	—	RingHomInvPair.ids
freeLift_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory free freeLift ModuleCat.ofHom Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero ModuleCat.carrier Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Finsupp.linearCombination DFunLike.coe LinearMap Action.V instAddCommGroupCarrierVModuleCat LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ LinearEquiv.toLinearMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearEquiv.symm Finsupp.curryLinearEquiv	—	—
freeLift_hom_single_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory free ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom freeLift Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCarrierVModuleCat DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	Finsupp.uncurry_single Finsupp.linearCombination_single
free_ext 📖	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory free ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	LinearEquiv.injective RingHomInvPair.ids
free_ext_iff 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory free ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	free_ext
free_projective 📖	mathematical	—	CategoryTheory.Projective Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory free	—	CategoryTheory.Adjunction.projective_of_map_projective CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor ModuleCat.projective_of_free
homEquiv_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory ihom DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory EquivLike.toFunLike Equiv.instEquivLike homEquiv ModuleCat.ofHom ModuleCat.carrier LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule ModuleCat.isAddCommGroup LinearMap.addCommGroup LinearMap.module LinearMap.flip CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence Ring.toSemiring TensorProduct.curry ModuleCat.Hom.hom	—	—
homEquiv_def 📖	mathematical	—	CategoryTheory.Adjunction.homEquiv Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.tensorLeft Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed instMonoidalClosed CategoryTheory.ihom.adjunction homEquiv	—	CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
homEquiv_symm_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj ihom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv ModuleCat.ofHom TensorProduct CommRing.toCommSemiring ModuleCat.carrier CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule TensorProduct.addCommGroup TensorProduct.instModule LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module TensorProduct.addCommMonoid LinearMap.instFunLike TensorProduct.uncurry LinearMap.flip Ring.toSemiring Action.V instAddCommGroupCarrierVModuleCat ModuleCat.Hom.hom	—	—
hom_comm_apply 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CommSemiring.toSemiring CommRing.toCommSemiring instAddCommGroupCarrierVModuleCat Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	LinearMap.ext_iff ModuleCat.hom_ext_iff Action.Hom.comm
ihom_coev_app_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed instMonoidalClosed CategoryTheory.NatTrans.app CategoryTheory.ihom.coev ModuleCat.ofHom ModuleCat.carrier LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule ModuleCat.isAddCommGroup LinearMap.addCommGroup LinearMap.module LinearMap.flip TensorProduct CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid	—	ModuleCat.hom_ext TensorProduct.smulCommClass_left smulCommClass_self LinearMap.ext
ihom_ev_app_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor.comp CategoryTheory.ihom Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.MonoidalClosed.closed instMonoidalClosed CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.ihom.ev ModuleCat.ofHom TensorProduct CommRing.toCommSemiring ModuleCat.carrier Action.V LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.instModule DFunLike.coe CommSemiring.toCommMonoid TensorProduct.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike TensorProduct.uncurry LinearMap.flip LinearMap.id	—	ModuleCat.hom_ext smulCommClass_self LinearMap.instSMulCommClass LinearMap.ext
ihom_map_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid of LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.addCommGroup ModuleCat.isAddCommGroup LinearMap.module Representation.linHom ρ CategoryTheory.Functor.map Rep Action.instCategory ihom ModuleCat.ofHom DFunLike.coe Ring.toSemiring LinearMap.addCommMonoid LinearMap.instFunLike LinearMap.llcomp ModuleCat.Hom.hom	—	—
ihom_obj_V_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory ihom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule	—	—
ihom_obj_V_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory ihom LinearMap.addCommGroup ModuleCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring	—	—
ihom_obj_V_isModule 📖	mathematical	—	ModuleCat.isModule CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory ihom LinearMap.module ModuleCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat RingHom.id Semiring.toNonAssocSemiring	—	—
ihom_obj_ρ 📖	mathematical	—	Action.ρ ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory ihom MonoidHom.comp LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.of CommSemiring.toSemiring CommRing.toCommSemiring Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.addCommGroup ModuleCat.isAddCommGroup LinearMap.module 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 Representation.linHom ρ	—	—
ihom_obj_ρ_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ CategoryTheory.Functor.obj Rep Action.instCategory ihom LinearMap.comp RingHomCompTriple.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smulCommClass_self
ihom_obj_ρ_def 📖	mathematical	—	ρ DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.ihom Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.MonoidalClosed.closed instMonoidalClosed ihom	—	—
instEnoughProjectives 📖	mathematical	—	CategoryTheory.EnoughProjectives Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Equivalence.enoughProjectives_iff ModuleCat.enoughProjectives UnivLE.small UnivLE.self
instEpiModuleCatHom 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory Action.V Action.Hom.hom	—	CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV
instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ 📖	mathematical	—	Representation.IsTrivial ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule MonoidHom.comp LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
instIsTrivialObjModuleCatTrivialFunctor 📖	mathematical	—	IsTrivial CategoryTheory.Functor.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory Rep Action.instCategory trivialFunctor	—	—
instIsTrivialOfOfIsTrivial 📖	mathematical	—	IsTrivial of	—	Representation.isTrivial_def
instIsTrivialTrivial 📖	mathematical	—	IsTrivial trivial	—	Representation.isTrivial_def Representation.instIsTrivialTrivial
instMonoModuleCatHom 📖	mathematical	—	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory Action.V Action.Hom.hom	—	CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV
instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV 📖	mathematical	—	CategoryTheory.Limits.PreservesColimits Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV	—	Action.preservesColimits_forget ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self
instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV	—	Action.preservesLimits_forget ModuleCat.hasLimits'
leftRegularHomEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory leftRegular ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive instAddCommGroupCarrierVModuleCat CategoryTheory.Linear.homModule instLinearRep ModuleCat.isModule EquivLike.toFunLike LinearEquiv.instEquivLike leftRegularHomEquiv CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids
leftRegularHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory leftRegular AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive ModuleCat.isModule CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm leftRegularHomEquiv leftRegularHom	—	RingHomInvPair.ids
leftRegularHomEquiv_symm_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory leftRegular ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory instAddCommGroupCarrierVModuleCat CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm leftRegularHomEquiv Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne 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 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory leftRegular leftRegularHom ModuleCat.ofHom Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ModuleCat.carrier Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule ModuleCat.isAddCommGroup ModuleCat.isModule DFunLike.coe AddEquiv LinearMap RingHom.id Action.V Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike Finsupp.lift LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
leftRegularHom_hom_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory leftRegular ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom leftRegularHom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCarrierVModuleCat DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	Finsupp.sum_single_index zero_smul
leftRegularTensorTrivialIsoFree_hom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule free CategoryTheory.Iso.hom leftRegularTensorTrivialIsoFree ModuleCat.ofHom TensorProduct NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instZero TensorProduct.addCommGroup TensorProduct.instModule LinearEquiv.toLinearMap Ring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid LinearEquiv.trans TensorProduct.addCommMonoid finsuppTensorFinsupp' Finsupp.domLCongr Equiv.prodComm Finsupp.curryLinearEquiv	—	—
leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat ModuleCat.moduleCategory ModuleCat.MonoidalCategory.instMonoidalCategoryStruct ModuleCat.of Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Finsupp.instZero AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommMonoid ModuleCat.isModule TensorProduct LinearMap.instFunLike ModuleCat.Hom.hom Action.V Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial free Action.Hom.hom CategoryTheory.Iso.hom leftRegularTensorTrivialIsoFree TensorProduct.tmul Finsupp.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	finsuppTensorFinsupp'_single_tmul_single Finsupp.equivMapDomain_single Finsupp.curry_single
leftRegularTensorTrivialIsoFree_inv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory free CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule CategoryTheory.Iso.inv leftRegularTensorTrivialIsoFree ModuleCat.ofHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instZero TensorProduct NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule LinearEquiv.toLinearMap Ring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid LinearEquiv.trans LinearEquiv.symm Finsupp.curryLinearEquiv Finsupp.domLCongr Equiv.prodComm finsuppTensorFinsupp'	—	LinearEquiv.trans.congr_simp Finsupp.domLCongr_symm
leftRegularTensorTrivialIsoFree_inv_hom_single_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero ModuleCat.carrier CommRing.toRing CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat ModuleCat.moduleCategory ModuleCat.MonoidalCategory.instMonoidalCategoryStruct ModuleCat.of Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom Action.V free Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory leftRegular trivial Action.Hom.hom CategoryTheory.Iso.inv leftRegularTensorTrivialIsoFree Finsupp.single TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	LinearEquiv.trans.congr_simp Finsupp.domLCongr_symm Finsupp.uncurry_single Finsupp.equivMapDomain_single finsuppTensorFinsupp'_symm_single_eq_tmul_single_one
leftRegular_projective 📖	mathematical	—	CategoryTheory.Projective Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory leftRegular	—	CategoryTheory.Projective.of_iso diagonal_succ_projective
linearizationTrivialIso_hom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid instOneMonoidHom trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule CategoryTheory.Iso.hom linearizationTrivialIso CategoryTheory.CategoryStruct.id Action.V	—	—
linearizationTrivialIso_inv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory trivial Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid instOneMonoidHom CategoryTheory.Iso.inv linearizationTrivialIso CategoryTheory.CategoryStruct.id Action.V	—	—
linearization_map_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization CategoryTheory.Functor.map ModuleCat.ofHom Finsupp Action.V AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toModule Finsupp.lmapDomain	—	—
linearization_map_hom_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Functor.map Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finsupp.mapDomain_single
linearization_obj_ρ 📖	mathematical	—	DFunLike.coe Representation ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Finsupp.lmapDomain NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.monoid Action.ρ	—	—
linearization_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.monoid Action.ρ	—	Finsupp.mapDomain_single
linearization_δ_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalActionTypeLinearization ModuleCat.ofHom Finsupp Action.V MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring TensorProduct Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Finsupp.instAddCommGroup Ring.toAddCommGroup TensorProduct.addCommGroup TensorProduct.instModule LinearEquiv.toLinearMap RingHom.id RingHomInvPair.ids TensorProduct.addCommMonoid LinearEquiv.symm finsuppTensorFinsupp'	—	—
linearization_ε_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.Functor.obj Action CategoryTheory.types linearization CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalActionTypeLinearization ModuleCat.ofHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Semiring.toModule Ring.toSemiring Finsupp.instAddCommGroup Finsupp.module Finsupp.lsingle	—	—
linearization_η_hom_apply 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action CategoryTheory.types Action.instCategory Rep linearization CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory ModuleCat.monoidalCategory ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalActionTypeLinearization Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	CategoryTheory.Iso.hom_inv_id_apply
linearization_μ_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.Functor.obj Action CategoryTheory.types linearization CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalActionTypeLinearization ModuleCat.ofHom TensorProduct CommRing.toCommSemiring Finsupp Action.V MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup TensorProduct.instModule LinearEquiv.toLinearMap RingHom.id RingHomInvPair.ids TensorProduct.addCommMonoid finsuppTensorFinsupp'	—	—
mkQ_hom 📖	mathematical	Submodule ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule 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 ρ	Action.Hom.hom quotient mkQ ModuleCat.ofHom HasQuotient.Quotient ModuleCat.isAddCommGroup Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module Submodule.mkQ	—	—
mono_iff_injective 📖	mathematical	—	CategoryTheory.Mono Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory ModuleCat.carrier Action.V DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom	—	ModuleCat.mono_iff_injective CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.forget₂_faithful
normNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.id normNatTrans norm	—	—
norm_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory norm	—	Action.hom_ext ModuleCat.hom_ext LinearMap.ext LinearMap.coe_sum Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr hom_comm_apply
norm_comm_apply 📖	mathematical	—	DFunLike.coe Action.HomSubtype ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CategoryTheory.ConcreteCategory.hom Rep Action.instCategory Action.instConcreteCategoryHomSubtypeV norm	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise norm_comm
norm_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory norm	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' norm_comm
norm_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid norm ModuleCat.ofHom ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Representation.norm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ρ	—	—
ofDistribMulAction_ρ_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory ofDistribMulAction AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule 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_ρ 📖	mathematical	—	ModuleCat.ofHom CommRing.toRing ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory ModuleCat.isAddCommGroup ModuleCat.isModule DFunLike.coe Representation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.monoid Action.ρ	—	—
ofModuleMonoidAlgebra_obj_coe 📖	mathematical	—	ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj MonoidAlgebra CommSemiring.toSemiring CommRing.toCommSemiring MonoidAlgebra.ring Rep Action.instCategory ofModuleMonoidAlgebra RestrictScalars	—	—
ofModuleMonoidAlgebra_obj_ρ 📖	mathematical	—	ρ CategoryTheory.Functor.obj ModuleCat MonoidAlgebra CommSemiring.toSemiring CommRing.toCommSemiring MonoidAlgebra.ring CommRing.toRing ModuleCat.moduleCategory Rep Action.instCategory ofModuleMonoidAlgebra Representation.ofModule ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	—
ofMulActionSubsingletonIsoTrivial_hom_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory ofMulAction trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Iso.hom Rep Action.instCategory ofMulActionSubsingletonIsoTrivial ModuleCat.ofHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp.LinearEquiv.finsuppUnique uniqueOfSubsingleton MulOne.toOne MulOneClass.toMulOne	—	—
ofMulActionSubsingletonIsoTrivial_inv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring ofMulAction CategoryTheory.Iso.inv Rep Action.instCategory ofMulActionSubsingletonIsoTrivial ModuleCat.ofHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring LinearEquiv.symm Finsupp.LinearEquiv.finsuppUnique uniqueOfSubsingleton MulOne.toOne MulOneClass.toMulOne	—	—
ofMulDistribMulAction_ρ_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory ofMulDistribMulAction AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule 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_ρ 📖	mathematical	—	ρ of	—	—
res_obj_ρ 📖	mathematical	—	ρ CategoryTheory.Functor.obj Action ModuleCat CommRing.toRing ModuleCat.moduleCategory Action.instCategory Action.res MonoidHom.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—
subtype_hom 📖	mathematical	Submodule ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule 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 ρ	Action.Hom.hom subrepresentation subtype ModuleCat.ofHom SetLike.instMembership Submodule.setLike Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module Submodule.subtype	—	—
tensor_ρ 📖	mathematical	—	ρ CategoryTheory.MonoidalCategoryStruct.tensorObj Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory Representation.tprod ModuleCat.carrier Action.V CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule	—	—
toAdditive_apply 📖	mathematical	—	DFunLike.coe AddEquiv ModuleCat.carrier CommRing.toRing Int.instCommRing Action.V ModuleCat ModuleCat.moduleCategory ofMulDistribMulAction Additive AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat 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 ModuleCat.carrier CommRing.toRing Int.instCommRing Action.V ModuleCat ModuleCat.moduleCategory ofMulDistribMulAction Additive.add MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAdditive	—	—
to_Module_monoidAlgebra_map_aux 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe MonoidHom LinearMap MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike	LinearMap.instFunLike AlgHom MonoidAlgebra MonoidAlgebra.semiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike MonoidAlgebra.lift	—	RingHomCompTriple.ids MonoidAlgebra.induction_on smulCommClass_self IsScalarTower.left MonoidAlgebra.lift_single one_smul LinearMap.congr_fun map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass
trivialFunctor_map_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory trivial ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.Functor.map Rep Action.instCategory trivialFunctor	—	—
trivialFunctor_obj_V 📖	mathematical	—	Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory trivialFunctor	—	—
trivial_def 📖	mathematical	—	DFunLike.coe Representation ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory trivial CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ LinearMap.id	—	—
trivial_projective_of_subsingleton 📖	mathematical	—	CategoryTheory.Projective Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	—	CategoryTheory.Projective.of_iso diagonal_succ_projective
unit_iso_comm 📖	mathematical	—	DFunLike.coe AddEquiv ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor.comp MonoidAlgebra CommSemiring.toSemiring CommRing.toCommSemiring MonoidAlgebra.ring toModuleMonoidAlgebra ofModuleMonoidAlgebra AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat EquivLike.toFunLike AddEquiv.instEquivLike unitIsoAddEquiv AddHom.toFun LinearMap.toAddHom RingHom.id Semiring.toNonAssocSemiring ModuleCat.isModule Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	RingHomInvPair.ids Representation.asModuleEquiv_symm_map_rho Representation.single_smul LinearEquiv.apply_symm_apply one_smul Representation.ofModule_asModule_act AddEquiv.apply_symm_apply
ρ_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ Representation ModuleCat.carrier CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—

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	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.ihom Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearHomEquivComm ModuleCat.ofHom ModuleCat.carrier CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence LinearMap Ring.toSemiring Action.V ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.addCommGroup LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.curry ModuleCat.Hom.hom	—	RingHomInvPair.ids
linearHomEquivComm_symm_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearHomEquivComm ModuleCat.ofHom TensorProduct ModuleCat.carrier Action.V Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.instModule LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike TensorProduct.uncurry ModuleCat.Hom.hom	—	ModuleCat.hom_ext RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass TensorProduct.ext'
linearHomEquiv_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.ihom Action.instMonoidalCategory ModuleCat.monoidalCategory CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearHomEquiv ModuleCat.ofHom ModuleCat.carrier CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Action.functorCategoryEquivalence LinearMap Ring.toSemiring Action.V ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.addCommGroup LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.flip TensorProduct.curry ModuleCat.Hom.hom	—	RingHomInvPair.ids
linearHomEquiv_symm_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed Rep.instMonoidalClosed AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearHomEquiv ModuleCat.ofHom TensorProduct ModuleCat.carrier Action.V Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule TensorProduct.addCommGroup ModuleCat.isAddCommGroup TensorProduct.instModule LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike TensorProduct.uncurry LinearMap.flip Ring.toSemiring ModuleCat.Hom.hom	—	RingHomInvPair.ids smulCommClass_self LinearMap.instSMulCommClass Rep.homEquiv_def

Representation

Definitions

Name	Category	Theorems
repOfTprodIso 📖	CompOp	2 math math: repOfTprodIso_inv_apply, repOfTprodIso_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
repOfTprodIso_apply 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory Rep.of TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tprod CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.hom repOfTprodIso	—	—
repOfTprodIso_inv_apply 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.MonoidalCategoryStruct.tensorObj Rep Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory ModuleCat.monoidalCategory Rep.of TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tprod ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom CategoryTheory.Iso.inv repOfTprodIso	—	—

(root)

Definitions

Name	Category	Theorems
Rep 📖	CompOp	279 math math: Rep.resCoindHomEquiv_symm_apply_hom, Representation.repOfTprodIso_inv_apply, Rep.resCoindHomEquiv_apply_hom, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Rep.coe_linearization_obj_ρ, groupHomology.mapCycles₂_comp_assoc, Rep.MonoidalClosed.linearHomEquiv_symm_hom, groupHomology.coinfNatTrans_app, groupHomology.mapShortComplexH2_id, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, Rep.diagonalSuccIsoFree_inv_hom_single, Representation.repOfTprodIso_apply, Rep.coindResAdjunction_counit_app, groupHomology.mapCycles₁_comp_apply, groupHomology.mapShortComplexH1_zero, groupHomology.cyclesMap_id_comp, Rep.indFunctor_obj, groupHomology.mapShortComplexH2_zero, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, Rep.indCoindNatIso_hom_app, groupHomology.chainsMap_id, Rep.invariantsFunctor_obj_carrier, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Rep.barComplex.d_def, Rep.diagonalHomEquiv_symm_apply, Rep.coindFunctor_map, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, Rep.instIsRightAdjointCoindFunctor, groupHomology.mapCycles₁_comp_assoc, Rep.instIsTrivialObjModuleCatTrivialFunctor, Rep.coinvariantsAdjunction_counit_app, groupHomology.map_id, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, Rep.linearization_single, groupHomology.coresNatTrans_app, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Rep.standardComplex.d_eq, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, groupHomology.π_comp_H0Iso_hom_assoc, Rep.trivial_projective_of_subsingleton, Rep.homEquiv_apply_hom, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, Rep.norm_comm_apply, Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom, Rep.indCoindIso_inv_hom_hom, Rep.free_projective, Rep.diagonalSuccIsoFree_inv_hom_single_single, groupHomology.mapCycles₁_id_comp_assoc, Rep.instLinearModuleCatObjFunctorCoinvariantsTensor, groupHomology.mapCycles₁_comp, groupHomology.map_comp, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.ihom_ev_app_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, Rep.coe_linearization_obj, Rep.instIsRightAdjointModuleCatInvariantsFunctor, groupHomology.map_id_comp, Rep.coinvariantsTensorIndIso_inv, groupHomology.functor_obj, Rep.standardComplex.εToSingle₀_comp_eq, Rep.homEquiv_def, Rep.indCoindIso_hom_hom_hom, 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.coinvariantsFunctor_obj_carrier, Rep.applyAsHom_comm_apply, Rep.instProjective, Rep.coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, Rep.coinvariantsTensorIndIso_hom, Rep.barResolution_complex, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, Rep.coinvariantsTensorIndNatIso_inv_app, Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor, Rep.coindResAdjunction_unit_app, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.map_id, Rep.indResAdjunction_counit_app_hom_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, Rep.resIndAdjunction_homEquiv_symm_apply, Rep.instLinearModuleCatCoinvariantsFunctor, Rep.normNatTrans_app, groupHomology.π_comp_H0Iso_hom_apply, Rep.applyAsHom_comm_assoc, Rep.freeLiftLEquiv_apply, groupHomology.chainsFunctor_obj, Rep.instEnoughProjectives, groupCohomology.functor_obj, Rep.ihom_obj_ρ_apply, Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.finsuppTensorRight_hom_hom, groupCohomology.resNatTrans_app, Rep.tensor_ρ, Rep.resIndAdjunction_homEquiv_apply, groupHomology.mapCycles₂_comp_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.linearization_η_hom_apply, Rep.quotientToInvariantsFunctor_map_hom, groupHomology.chainsMap_id_comp, Rep.leftRegularHomEquiv_symm_apply, Rep.quotientToCoinvariantsFunctor_map_hom, groupCohomology.mapShortComplexH1_id, Rep.coinvariantsShortComplex_g, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, Rep.coindResAdjunction_homEquiv_apply, Rep.Tor_map, Rep.ofModuleMonoidAlgebra_obj_ρ, Rep.coinvariantsShortComplex_f, Rep.resIndAdjunction_counit_app, Rep.ofMulActionSubsingletonIsoTrivial_inv_hom, Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor, Representation.coind'_apply_apply, Rep.diagonalOneIsoLeftRegular_inv_hom, groupHomology.map_id_comp_H0Iso_hom_assoc, groupHomology.mapCycles₂_id_comp_assoc, Rep.coindIso_inv_hom_hom, groupHomology.mapShortComplexH2_comp, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.mapCycles₁_id_comp, Rep.trivialFunctor_obj_V, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.linearization_obj_ρ, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, Rep.invariantsAdjunction_counit_app_hom, groupHomology.chainsMap_comp, Rep.instLinearModuleCatInvariantsFunctor, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Rep.ofMulActionSubsingletonIsoTrivial_hom_hom, Rep.linearizationTrivialIso_inv_hom, Rep.isZero_Tor_succ_of_projective, Rep.quotientToInvariantsFunctor_obj_V, Rep.coinvariantsTensorIndNatIso_hom_app, groupHomology.congr, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, Rep.applyAsHom_comm, Rep.standardComplex.d_comp_ε, Rep.finsuppTensorRight_inv_hom, Rep.ihom_obj_V_isAddCommGroup, Rep.indCoindNatIso_inv_app, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, Rep.coindResAdjunction_homEquiv_symm_apply, groupHomology.pOpcycles_comp_opcyclesIso_hom, Rep.trivialFunctor_map_hom, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.mapShortComplexH1_id, Rep.ihom_map_hom, Rep.coinvariantsTensor_hom_ext_iff, Rep.finsuppTensorLeft_inv_hom, Rep.unit_iso_comm, Rep.leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, Rep.FiniteCyclicGroup.resolution_complex, groupHomology.chainsFunctor_map, Rep.leftRegularTensorTrivialIsoFree_inv_hom, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.indResAdjunction_unit_app_hom_hom, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.H1CoresCoinfOfTrivial_f, Rep.coindFunctor'_obj, Rep.linearization_δ_hom, groupHomology.functor_map, groupHomology.mapCycles₂_id_comp_apply, Rep.standardComplex.instQuasiIsoNatεToSingle₀, Rep.standardComplex.x_projective, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, Rep.FiniteCyclicGroup.resolution_quasiIso, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, groupCohomology.H1Map_id, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, Rep.finsuppTensorLeft_hom_hom, Rep.indFunctor_map, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.π_comp_H0Iso_hom, Rep.coinvariantsTensorMk_apply, groupHomology.H0π_comp_H0Iso_hom, Rep.coinvariantsShortComplex_X₁, Rep.homEquiv_symm_apply_hom, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, Rep.invariantsFunctor_map_hom, groupHomology.map_id_comp_H0Iso_hom, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.cocyclesMap_id, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, Rep.norm_comm_assoc, Rep.resIndAdjunction_unit_app, Rep.diagonalOneIsoLeftRegular_hom_hom, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.ihom_coev_app_hom, Rep.leftRegularHomEquiv_apply, Rep.leftRegular_projective, groupHomology.chainsMap_zero, groupHomology.mapShortComplexH2_id_comp, Rep.ihom_obj_V_isModule, groupCohomology.mapShortComplexH2_id, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, Rep.diagonalHomEquiv_apply, Rep.coinvariantsAdjunction_unit_app_hom, Rep.freeLiftLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, Rep.epi_iff_surjective, groupCohomology.cochainsFunctor_map, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Rep.coinvariantsShortComplex_X₂, groupHomology.H0π_comp_H0Iso_hom_assoc, groupHomology.cyclesMap_comp, Rep.indResHomEquiv_apply_hom, Rep.linearizationTrivialIso_hom_hom, Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, Rep.coinvariantsAdjunction_homEquiv_apply_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomology.H1CoresCoinf_f, Rep.diagonalSuccIsoFree_hom_hom_single, Rep.ihom_obj_ρ, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, Rep.instIsLeftAdjointIndFunctor, Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, Representation.linHom.invariantsEquivRepHom_apply_hom, groupHomology.cyclesMap_id, Rep.instAdditiveModuleCatInvariantsFunctor, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, Rep.coindFunctor'_map, Rep.coinvariantsFunctor_map_hom, Rep.coindFunctor_obj, Rep.linearization_map_hom_single, groupCohomology.map_id_comp_H0Iso_hom_assoc, Rep.ihom_obj_ρ_def, Rep.ihom_obj_V_carrier, Rep.coinvariantsShortComplex_X₃, Rep.coindIso_hom_hom_hom, Rep.leftRegularTensorTrivialIsoFree_hom_hom, groupHomology.H0π_comp_H0Iso_hom_apply, Rep.mono_iff_injective, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.functor_map, Rep.linearization_ε_hom, Rep.Tor_obj, Rep.coinvariantsShortComplex_shortExact, Rep.FiniteCyclicGroup.resolution_π, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.FiniteCyclicGroup.resolution.π_f, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Rep.instAdditiveModuleCatCoinvariantsFunctor, groupCohomology.cochainsFunctor_obj, Rep.linearization_map_hom, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, Rep.indResHomEquiv_symm_apply_hom, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, Rep.norm_comm, Rep.linearization_μ_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, Rep.quotientToCoinvariantsFunctor_obj_V, groupCohomology.cochainsMap_id, Rep.instInjective
instLinearRep 📖	CompOp	35 math math: Rep.resCoindHomEquiv_symm_apply_hom, Rep.resCoindHomEquiv_apply_hom, Rep.MonoidalClosed.linearHomEquiv_symm_hom, Rep.diagonalHomEquiv_symm_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, Rep.instLinearModuleCatObjFunctorCoinvariantsTensor, Rep.MonoidalClosed.linearHomEquivComm_hom, Rep.coindVEquiv_symm_apply_coe, Rep.resIndAdjunction_homEquiv_symm_apply, Rep.instLinearModuleCatCoinvariantsFunctor, Rep.coindMap'_hom, Rep.freeLiftLEquiv_apply, Rep.resIndAdjunction_homEquiv_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.leftRegularHomEquiv_symm_apply, Rep.coindResAdjunction_homEquiv_apply, Representation.coind'_apply_apply, Rep.coindIso_inv_hom_hom, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.instLinearModuleCatInvariantsFunctor, Rep.coindResAdjunction_homEquiv_symm_apply, Rep.coindVEquiv_apply_hom, Rep.leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, Rep.leftRegularHomEquiv_apply, Rep.diagonalHomEquiv_apply, Rep.freeLiftLEquiv_symm_apply, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Rep.indResHomEquiv_apply_hom, Representation.linHom.invariantsEquivRepHom_apply_hom, Rep.coindIso_hom_hom_hom, Rep.indResHomEquiv_symm_apply_hom

---

← Back to Index