Cochain

📁 Source: Mathlib/Algebra/Lie/Cochain.lean

Statistics

Metric	Count
Definitions Cochain, d₁₂, d₂₃, instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain, oneCochain, twoCochain, twoCocycle	7
Theorems add_apply_apply, d₁₂_apply_apply, d₁₂_apply_apply_ofTrivial, d₁₂_apply_coe_apply_apply, d₂₃_apply, d₂₃_comp_d₁₂, instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, mem_twoCochain_iff, mem_twoCocycle_iff, mem_twoCocycle_iff_of_trivial, smul_apply_apply, twoCochain_alt, twoCochain_skew, twoCochain_val_apply	14
Total	21

CochainComplex.HomComplex

Definitions

Name	Category	Theorems
Cochain 📖	CompOp	203 math math: δ_units_smul, Cochain.rightShiftAddEquiv_symm_apply, Cochain.fromSingleMk_neg, Cocycle.precomp_coe, CochainComplex.mappingCocone.inr_v_snd_v_assoc, Cochain.δ_single, CochainComplex.Lifting.π_f_cochain₁_v_ι_f, Cocycle.coe_smul, CochainComplex.mappingCone.id, Cochain.InductionUp.limitSequence_eqUpTo, CochainComplex.mappingCone.inr_f_fst_v, Cochain.leftShift_smul, CochainComplex.mappingCocone.inr_v_snd_v, Cochain.fromSingleEquiv_fromSingleMk, CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero, Cocycle.coe_sub, Cocycle.toCochainAddMonoidHom_apply, δ_neg, CochainComplex.mappingCone.d_snd_v, Cochain.rightUnshift_neg, CochainComplex.mappingCone.inl_snd_assoc, Cochain.InductionUp.sequence_eqUpTo, Cocycle.postcomp_coe, Cocycle.coe_units_smul, Cochain.units_smul_comp, Cochain.shift_add, Cochain.toSingleMk_neg, CochainComplex.mappingCone.liftCochain_descCochain, Cochain.comp_neg, Cochain.map_zero, leftHomologyData'_i, CochainComplex.mappingCone.liftCocycle_coe, Cochain.leftShiftLinearEquiv_apply, Cochain.shift_neg, Cochain.toSingleMk_add, Cochain.neg_v, Cochain.sub_v, CochainComplex.mappingCone.lift_f_fst_v, CochainComplex.Lifting.exists_hom, Cochain.rightUnshift_units_smul, CochainComplex.mappingCone.id_X, Cochain.single_zero, CochainComplex.mappingCocone.inr_v_desc_f_assoc, Cochain.comp_add, Cochain.neg_comp, leftHomologyData_i_hom_apply, CochainComplex.mappingCone.d_snd_v'_assoc, Cochain.shift_zero, Cochain.leftShift_comp, δ_zero, Cochain.add_comp, Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, CochainComplex.mappingCone.lift_f_fst_v_assoc, CochainComplex.mappingCocone.id_X, CochainComplex.mappingCocone.descCocycle_coe, Cochain.leftShift_rightShift, Cochain.ofHom_neg, Cochain.zero_v, δ_ofHom, CochainComplex.mappingCocone.inr_comp_descCochain, Cochain.map_add, Cocycle.cochain_ofHom_homOf_eq_coe, Cochain.fromSingleMk_add, Cochain.shift_smul, Cochain.leftShiftAddEquiv_apply, Cochain.ofHomotopy_refl, Cochain.rightShiftAddEquiv_apply, Cocycle.coe_neg, CochainComplex.mappingCone.inl_snd, Cochain.rightShift_leftShift, Cochain.ofHom_sub, Cochain.leftUnshift_smul, Cochain.shiftLinearMap_apply, CochainComplex.mappingCone.ofHom_lift, Cocycle.toSingleMk_coe, CochainComplex.mappingCocone.ofHom_desc, CochainComplex.mappingCone.ext_to_iff, Cochain.rightShift_zero, CochainComplex.mappingCone.lift_fst, CochainComplex.mappingCone.ext_cochain_to_iff, δ_smul, CochainComplex.mappingCone.liftCochain_v_fst_v, Cochain.fromSingleMk_zero, CochainComplex.mappingCone.decomp_from, δ_comp, Cochain.leftShift_zero, mem_coboundaries_iff, Cocycle.fromSingleMk_coe, CochainComplex.mappingCone.descCocycle_coe, Cochain.smul_comp, Cocycle.leftUnshift_coe, Cochain.equivHomotopy_apply_of_eq, CochainComplex.mappingCone.d_snd_v_assoc, δ_add, CochainComplex.mappingCone.d_snd_v', Cochain.rightShift_smul, CochainComplex.mappingCone.liftCochain_fst, Cochain.map_sub, Cocycle.homOf_f, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.homOfDegreewiseSplit_f, Cocycle.δ_eq_zero, CochainComplex.mappingCone.δ_snd, CochainComplex.mappingCone.inl_v_fst_v, CochainComplex.Lifting.π_f_cochain₁_v_ι_f_assoc, Cochain.shift_units_smul, δ_hom_apply, Cochain.leftShiftLinearEquiv_symm_apply, CochainComplex.mappingCocone.inr_v_fst_f_assoc, Cochain.units_smul_v, Cochain.δ_toSingleMk, Cochain.leftUnshift_add, CochainComplex.mappingCone.inr_f_fst_v_assoc, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, Cochain.rightShift_units_smul, Cochain.rightUnshift_smul, Cochain.smul_v, Cochain.δ_shift, Cochain.fromSingleMk_sub, Cochain.comp_units_smul, Cochain.δ_rightUnshift, Cochain.comp_sub, δ_δ, Cochain.leftUnshift_units_smul, CochainComplex.mappingCone.inl_fst, Cochain.rightShiftLinearEquiv_apply, Cocycle.shift_coe, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, CochainComplex.mappingCone.lift_desc_f, CochainComplex.mappingCone.δ_liftCochain, Cochain.δ_rightShift, CochainComplex.mappingCone.desc_f, CochainComplex.mappingCone.d_fst_v'_assoc, CochainComplex.mappingCocone.inr_v_fst_f, Cochain.rightUnshift_add, Cochain.toSingleMk_zero, Cochain.shiftAddHom_apply, Cochain.δ_leftUnshift, CochainComplex.mappingCone.d_fst_v', Cochain.leftShift_add, CochainComplex.mappingCocone.δ_descCochain, CochainComplex.HomComplex_X, CochainComplex.mappingCone.inl_fst_assoc, Cocycle.ext_iff, Cocycle.ofHom_coe, δ_shape, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, Cochain.leftShift_units_smul, Cochain.equivHomotopy_apply_coe, δ_comp_zero_cocycle, Cocycle.coe_zero, Cochain.ofHom_add, Cochain.zero_comp, Cochain.ofHom_zero, CochainComplex.mappingCone.δ_descCochain, Cochain.comp_zero, Cochain.leftShiftAddEquiv_symm_apply, Cochain.rightShift_neg, δ_comp_zero_cochain, Cochain.comp_smul, CochainComplex.isKInjective_of_injective_aux, CochainComplex.mappingCocone.inr_v_descCochain_v_assoc, Cochain.equivHomotopy_symm_apply_hom, CochainComplex.mappingCocone.δ_liftCochain, δ_sub, CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero, Cochain.rightShiftLinearEquiv_symm_apply, Cochain.rightUnshift_zero, Cocycle.leftShift_coe, Cocycle.coe_add, Cochain.sub_comp, CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero_assoc, Cochain.rightShift_add, Cocycle.diff_coe, Cochain.toSingleEquiv_toSingleMk, Cochain.ofHoms_zero, CochainComplex.Lifting.comp_coe_cocycle₁_comp, CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero_assoc, Cocycle.rightUnshift_coe, CochainComplex.mappingCone.lift_f, Cochain.δ_leftShift, Cochain.add_v, CochainComplex.mappingCone.inl_v_fst_v_assoc, δ_zero_cochain_comp, CochainComplex.mappingCocone.inr_v_descCochain_v, Cochain.leftShift_neg, Cochain.toSingleMk_sub, CochainComplex.mappingCocone.liftCocycle_coe, Cocycle.mk_coe, Cochain.leftUnshift_neg, CochainComplex.mappingCone.inr_fst, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, δ_ofHomotopy, Cocycle.mem_iff, Cocycle.rightShift_coe, CochainComplex.mappingCone.d_fst_v, Cochain.leftUnshift_zero, Cochain.map_neg, CochainComplex.HomComplex_d_hom_apply, CochainComplex.mappingCone.inr_fst_assoc, CochainComplex.mappingCocone.inr_v_desc_f, δ_zero_cocycle_comp, Cochain.ofHomotopy_ofEq

LieModule.Cohomology

Definitions

Name	Category	Theorems
d₁₂ 📖	CompOp	5 math math: d₁₂_apply_apply, d₁₂_apply_coe_apply_apply, d₁₂_apply_apply_ofTrivial, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, d₂₃_comp_d₁₂
d₂₃ 📖	CompOp	3 math math: d₂₃_apply, mem_twoCocycle_iff, d₂₃_comp_d₁₂
instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain 📖	CompOp	11 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, twoCochain_alt, d₂₃_apply, d₁₂_apply_apply, twoCochain_skew, d₁₂_apply_apply_ofTrivial, add_apply_apply, smul_apply_apply, instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, twoCochain_val_apply, mem_twoCocycle_iff_of_trivial
oneCochain 📖	CompOp	7 math math: d₁₂_apply_apply, d₁₂_apply_coe_apply_apply, d₁₂_apply_apply_ofTrivial, LieAlgebra.LieEquiv.ofCoboundary_toFun, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, LieAlgebra.LieEquiv.ofCoboundary_invFun, d₂₃_comp_d₁₂
twoCochain 📖	CompOp	19 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, twoCochain_alt, d₂₃_apply, d₁₂_apply_apply, LieAlgebra.bracket_ofTwoCocycle, twoCochain_skew, d₁₂_apply_coe_apply_apply, mem_twoCochain_iff, d₁₂_apply_apply_ofTrivial, mem_twoCocycle_iff, add_apply_apply, smul_apply_apply, instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, twoCochain_val_apply, mem_twoCocycle_iff_of_trivial, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, LieAlgebra.Extension.twoCocycleOf_coe_coe, d₂₃_comp_d₁₂
twoCocycle 📖	CompOp	6 math math: LieAlgebra.bracket_ofTwoCocycle, mem_twoCocycle_iff, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, mem_twoCocycle_iff_of_trivial, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, LieAlgebra.Extension.twoCocycleOf_coe_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain Submodule.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self LinearMap.instSMulCommClass
d₁₂_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain oneCochain Submodule.addCommMonoid Submodule.module d₁₂ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	smulCommClass_self LinearMap.instSMulCommClass
d₁₂_apply_apply_ofTrivial 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain oneCochain Submodule.addCommMonoid Submodule.module d₁₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	smulCommClass_self LinearMap.instSMulCommClass trivial_lie_zero sub_self zero_sub
d₁₂_apply_coe_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Submodule SetLike.instMembership Submodule.setLike twoCochain oneCochain smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.addCommMonoid Submodule.module d₁₂ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	smulCommClass_self LinearMap.instSMulCommClass
d₂₃_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule SetLike.instMembership Submodule.setLike twoCochain Submodule.addCommMonoid Submodule.module d₂₃ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Bracket.bracket LieRingModule.toBracket instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain lieRingSelfModule	—	smulCommClass_self LinearMap.instSMulCommClass
d₂₃_comp_d₁₂ 📖	mathematical	—	LinearMap.comp oneCochain LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain Submodule.addCommMonoid Submodule.module RingHomCompTriple.ids d₂₃ d₁₂ LinearMap.instZero	—	LinearMap.ext smulCommClass_self LinearMap.instSMulCommClass RingHomCompTriple.ids lie_sub lie_lie leibniz_lie instIsLieTower lie_skew lie_neg map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass sub_add_cancel map_sub Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg add_zero
instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain 📖	mathematical	—	LinearMapClass LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain	—	smulCommClass_self LinearMap.instSMulCommClass LinearMap.map_add LinearMap.map_smul
mem_twoCochain_iff 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain DFunLike.coe LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smulCommClass_self LinearMap.instSMulCommClass
mem_twoCocycle_iff 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain Submodule.addCommMonoid Submodule.module twoCocycle DFunLike.coe LinearMap.instFunLike d₂₃ LinearMap.instZero	—	smulCommClass_self LinearMap.instSMulCommClass
mem_twoCocycle_iff_of_trivial 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain Submodule.addCommMonoid Submodule.module twoCocycle DFunLike.coe LinearMap.instFunLike instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain Bracket.bracket LieRingModule.toBracket lieRingSelfModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self LinearMap.instSMulCommClass mem_twoCocycle_iff twoCochain_skew sub_eq_zero trivial_lie_zero sub_self add_zero zero_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat LinearMap.ext Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
smul_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain Submodule.smul Algebra.toSMul Algebra.id LinearMap.instSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.addCommGroup LinearMap.instDistribMulAction LinearMap.instIsScalarTower IsScalarTower.left SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass	—	smulCommClass_self LinearMap.instSMulCommClass LinearMap.instIsScalarTower IsScalarTower.left
twoCochain_alt 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smulCommClass_self LinearMap.instSMulCommClass
twoCochain_skew 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain	—	smulCommClass_self LinearMap.instSMulCommClass neg_eq_iff_add_eq_zero add_comm map_add SemilinearMapClass.toAddHomClass instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain LinearMap.semilinearMapClass twoCochain_alt zero_add add_zero
twoCochain_val_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike twoCochain instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain	—	smulCommClass_self LinearMap.instSMulCommClass

---

← Back to Index