Torsion

📁 Source: FLT/EllipticCurve/Torsion.lean

Statistics

Metric	Count
Definitions map, galoisRep, galoisRepresentation, galoisRepresentation_smul, n_torsion, instModuleZModN_torsion	6
Theorems map_comp, map_id, n_torsion_card, n_torsion_dimension, n_torsion_finite, group_theory_lemma, instFiniteZModN_torsion	7
Total	13
⚠️ With sorry galoisRep, n_torsion_card, n_torsion_finite, group_theory_lemma, instFiniteZModN_torsion	5

WeierstrassCurve

Definitions

Name	Category	Theorems
galoisRep 📖 ⚠️	CompOp	4 math math: FreyCurve.torsion_isHardlyRamified, Mazur_Frey, Wiles_Frey, FreyCurve.torsion_not_isIrreducible
galoisRepresentation 📖	CompOp	—
galoisRepresentation_smul 📖	CompOp	—
n_torsion 📖	CompOp	8 math math: instFiniteZModN_torsion, n_torsion_dimension, FreyCurve.torsion_isHardlyRamified, Mazur_Frey, n_torsion_finite, Wiles_Frey, n_torsion_card, FreyCurve.torsion_not_isIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
n_torsion_card 📖 ⚠️	mathematical	—	n_torsion	—	—
n_torsion_dimension 📖	mathematical	—	n_torsion	—	group_theory_lemma n_torsion_card
n_torsion_finite 📖 ⚠️	mathematical	—	n_torsion	—	—

WeierstrassCurve.Points

Definitions

Name	Category	Theorems
map 📖	CompOp	1 math math: map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	—	—	—	—	—
map_id 📖	mathematical	—	map	—	—

(root)

Definitions

Name	Category	Theorems
instModuleZModN_torsion 📖	CompOp	5 math math: instFiniteZModN_torsion, FreyCurve.torsion_isHardlyRamified, Mazur_Frey, Wiles_Frey, FreyCurve.torsion_not_isIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
group_theory_lemma 📖 ⚠️	—	—	—	—	—
instFiniteZModN_torsion 📖 ⚠️	mathematical	—	WeierstrassCurve.n_torsion instModuleZModN_torsion	—	—

---

← Back to Index