EulerCharacteristic

📁 Source: Mathlib/Algebra/Homology/EulerCharacteristic.lean

Statistics

Metric	Count
Definitions EulerCharSigns, χ, eulerCharSignsDownInt, eulerCharSignsDownNat, eulerCharSignsUpInt, eulerCharSignsUpNat, χ, eulerChar, finrankSupport, eulerChar, homologyEulerChar	11
Theorems χ_next, eulerCharSignsDownInt_χ, eulerCharSignsDownNat_χ, eulerCharSignsUpInt_χ, eulerCharSignsUpNat_χ, χ_next, χ_prev, eulerChar_eq_sum_finSet_of_finrankSupport_subset, finrankSupport_subset_iff, eulerChar_eq_sum_finSet_of_finrankSupport_subset, homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset	11
Total	22

ComplexShape

Definitions

Name	Category	Theorems
EulerCharSigns 📖	CompData	—
eulerCharSignsDownInt 📖	CompOp	1 math math: eulerCharSignsDownInt_χ
eulerCharSignsDownNat 📖	CompOp	1 math math: eulerCharSignsDownNat_χ
eulerCharSignsUpInt 📖	CompOp	1 math math: eulerCharSignsUpInt_χ
eulerCharSignsUpNat 📖	CompOp	1 math math: eulerCharSignsUpNat_χ
χ 📖	CompOp	5 math math: χ_prev, HomologicalComplex.eulerChar_eq_sum_finSet_of_finrankSupport_subset, χ_next, GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset, HomologicalComplex.homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eulerCharSignsDownInt_χ 📖	mathematical	—	EulerCharSigns.χ down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing eulerCharSignsDownInt Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd
eulerCharSignsDownNat_χ 📖	mathematical	—	EulerCharSigns.χ down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne eulerCharSignsDownNat Units Int.instMonoid Int.instUnitsPow Nat.instCommSemiring AddCommMonoid.toNatModule Additive Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
eulerCharSignsUpInt_χ 📖	mathematical	—	EulerCharSigns.χ up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing eulerCharSignsUpInt Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd
eulerCharSignsUpNat_χ 📖	mathematical	—	EulerCharSigns.χ up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne eulerCharSignsUpNat Units Int.instMonoid Int.instUnitsPow Nat.instCommSemiring AddCommMonoid.toNatModule Additive Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
χ_next 📖	mathematical	Rel	χ Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	EulerCharSigns.χ_next
χ_prev 📖	mathematical	Rel	χ Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	χ_next neg_neg

ComplexShape.EulerCharSigns

Definitions

Name	Category	Theorems
χ 📖	CompOp	5 math math: χ_next, ComplexShape.eulerCharSignsDownNat_χ, ComplexShape.eulerCharSignsUpInt_χ, ComplexShape.eulerCharSignsDownInt_χ, ComplexShape.eulerCharSignsUpNat_χ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
χ_next 📖	mathematical	ComplexShape.Rel	χ Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—

GradedObject

Definitions

Name	Category	Theorems
eulerChar 📖	CompOp	1 math math: eulerChar_eq_sum_finSet_of_finrankSupport_subset
finrankSupport 📖	CompOp	1 math math: finrankSupport_subset_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eulerChar_eq_sum_finSet_of_finrankSupport_subset 📖	mathematical	Set Set.instHasSubset finrankSupport SetLike.coe Finset Finset.instSetLike	eulerChar Finset.sum Int.instAddCommMonoid Units.val Int.instMonoid ComplexShape.χ Module.finrank ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	finsum_eq_sum_of_support_subset
finrankSupport_subset_iff 📖	mathematical	—	Set Set.instHasSubset finrankSupport Module.finrank ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	Function.support_subset_iff'

HomologicalComplex

Definitions

Name	Category	Theorems
eulerChar 📖	CompOp	1 math math: eulerChar_eq_sum_finSet_of_finrankSupport_subset
homologyEulerChar 📖	CompOp	1 math math: homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eulerChar_eq_sum_finSet_of_finrankSupport_subset 📖	mathematical	Set Set.instHasSubset GradedObject.finrankSupport X ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive SetLike.coe Finset Finset.instSetLike	eulerChar Finset.sum Int.instAddCommMonoid Units.val Int.instMonoid ComplexShape.χ Module.finrank ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset
homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset 📖	mathematical	HasHomology ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive Set Set.instHasSubset GradedObject.finrankSupport homology SetLike.coe Finset Finset.instSetLike	homologyEulerChar Finset.sum Int.instAddCommMonoid Units.val Int.instMonoid ComplexShape.χ Module.finrank ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset

---

← Back to Index