Basic

📁 Source: ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean

Statistics

Metric	Count
Definitions coprime_decompose	1
Theorems coprime_decompose_apply, coprime_decompose_symm_apply	2
Total	3

Module.IsTorsionBy

Definitions

Name	Category	Theorems
coprime_decompose 📖	CompOp	3 math math: groupCohomology.injects_to_sylowCoh, coprime_decompose_apply, coprime_decompose_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_decompose_apply 📖	mathematical	—	coprime_decompose	—	—
coprime_decompose_symm_apply 📖	mathematical	—	coprime_decompose	—	—

---

← Back to Index