TrivialityCriterion

📁 Source: ClassFieldTheory/Cohomology/TrivialityCriterion.lean

Statistics

Metric	Count
Definitions	0
Theorems down_trivialCohomology, up_trivialCohomology, tateCohomology_of_trivialCohomology, trivialHomology_of_trivialCohomology, trivialCohomology_of_even_of_odd, trivialCohomology_of_even_of_odd_of_solvable	6
Total	6

Rep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tateCohomology_of_trivialCohomology 📖	mathematical	—	TrivialTateCohomology	—	TrivialCohomology.isZero isZero_of_trivialCohomology TrivialCohomology.res_subtype dimensionShift.down_trivialCohomology
trivialHomology_of_trivialCohomology 📖	mathematical	—	TrivialHomology	—	isZero_of_trivialTateCohomology tateCohomology_of_trivialCohomology TrivialCohomology.res_subtype

Rep.dimensionShift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
down_trivialCohomology 📖	mathematical	—	Rep.TrivialCohomology down	—	groupCohomology.trivialCohomology_of_even_of_odd Rep.isZero_of_injective
up_trivialCohomology 📖	mathematical	—	Rep.TrivialCohomology up	—	groupCohomology.trivialCohomology_of_even_of_odd Rep.isZero_of_injective

groupCohomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trivialCohomology_of_even_of_odd 📖	mathematical	Rep.res	Rep.TrivialCohomology	—	torsion_of_finite_of_neZero groupCohomology_Sylow Rep.isZero_of_trivialCohomology trivialCohomology_of_even_of_odd_of_solvable
trivialCohomology_of_even_of_odd_of_solvable 📖	mathematical	Rep.res	Rep.TrivialCohomology	—	solvable_ind inflation_restriction_mono inflation_restriction_exact Rep.isZero_ofEven_odd

---

← Back to Index