Frey

📁 Source: FLT/GaloisRepresentation/HardlyRamified/Frey.lean

Statistics

Metric	Count
Definitions instAlgebraPadicIntZMod_fLT, instDecidableEqAlgebraicClosureRat_fLT	2
Theorems torsion_isHardlyRamified, torsion_not_isIrreducible	2
Total	4
⚠️ With sorry torsion_isHardlyRamified, torsion_not_isIrreducible	2

FreyCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
torsion_isHardlyRamified 📖 ⚠️	mathematical	—	GaloisRepresentation.IsHardlyRamified FreyPackage.p FreyPackage.pp FreyPackage.hp_odd instAlgebraPadicIntZMod_fLT WeierstrassCurve.n_torsion FreyPackage.freyCurve instDecidableEqAlgebraicClosureRat_fLT instModuleZModN_torsion instFiniteZModN_torsion WeierstrassCurve.galoisRep instIsEllipticRatFreyCurve	—	FreyPackage.pp FreyPackage.hp_odd instFiniteZModN_torsion instIsEllipticRatFreyCurve FreyPackage.hppos
torsion_not_isIrreducible 📖 ⚠️	mathematical	—	GaloisRep.IsIrreducible WeierstrassCurve.n_torsion FreyPackage.freyCurve instDecidableEqAlgebraicClosureRat_fLT FreyPackage.p FreyPackage.pp instModuleZModN_torsion WeierstrassCurve.galoisRep instIsEllipticRatFreyCurve FreyPackage.hppos	—	FreyPackage.pp instIsEllipticRatFreyCurve FreyPackage.hppos

(root)

Definitions

Name	Category	Theorems
instAlgebraPadicIntZMod_fLT 📖	CompOp	1 math math: FreyCurve.torsion_isHardlyRamified
instDecidableEqAlgebraicClosureRat_fLT 📖	CompOp	2 math math: FreyCurve.torsion_isHardlyRamified, FreyCurve.torsion_not_isIrreducible

---

← Back to Index