Documentation Verification Report

FreyPackage

📁 Source: FLT/Basic/FreyPackage.lean

Statistics

Metric	Count
Definitions `FreyPackage`, `a`, `b`, `c`, `freyCurve`, `freyCurveInt`, `p`	7
Theorems `of_p_ge_5`, `b₂`, `b₄`, `c₄`, `c₄'`, `instIsEllipticRatFreyCurve`, `j`, `j_valuation_of_bad_prime`, `map`, `Δ`, `Δ'inv`, `gcdab_eq_gcdac`, `hFLT`, `ha0`, `ha4`, `hb0`, `hb2`, `hc0`, `hgcdab`, `hgcdac`, `hgcdbc`, `hp0`, `hp5`, `hp_odd`, `hppos`, `of_not_FermatLastTheorem`, `of_not_FermatLastTheorem_p_ge_5`, `pp`, `pow_add_pow_ne_pow_of_FermatLastTheorem`	29
Total	36

FermatLastTheorem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_p_ge_5` 📖	—	—	—	—	—

FreyCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`b₂` 📖	mathematical	—	`FreyPackage.freyCurve` `FreyPackage.b` `FreyPackage.p` `FreyPackage.a`	—	—
`b₄` 📖	mathematical	—	`FreyPackage.freyCurve` `FreyPackage.a` `FreyPackage.b` `FreyPackage.p`	—	—
`c₄` 📖	mathematical	—	`FreyPackage.freyCurve` `FreyPackage.a` `FreyPackage.p` `FreyPackage.b`	—	`b₂` `b₄`
`c₄'` 📖	mathematical	—	`FreyPackage.freyCurve` `FreyPackage.c` `FreyPackage.p` `FreyPackage.a` `FreyPackage.b`	—	`c₄` `FreyPackage.hFLT`
`instIsEllipticRatFreyCurve` 📖	mathematical	—	`FreyPackage.freyCurve`	—	`Δ` `FreyPackage.ha0` `FreyPackage.hb0` `FreyPackage.hc0`
`j` 📖	mathematical	—	`FreyPackage.freyCurve` `instIsEllipticRatFreyCurve` `FreyPackage.c` `FreyPackage.p` `FreyPackage.a` `FreyPackage.b`	—	`instIsEllipticRatFreyCurve` `Δ'inv` `c₄'`
`j_valuation_of_bad_prime` 📖	mathematical	`FreyPackage.a` `FreyPackage.b` `FreyPackage.c`	`FreyPackage.p` `FreyPackage.freyCurve` `instIsEllipticRatFreyCurve`	—	`FreyPackage.hFLT` `FreyPackage.hb0` `FreyPackage.ha0` `FreyPackage.hc0` `instIsEllipticRatFreyCurve` `j` `FreyPackage.hgcdac` `FreyPackage.hgcdbc` `FreyPackage.hp0`
`map` 📖	mathematical	—	`FreyPackage.freyCurveInt` `FreyPackage.freyCurve`	—	`FreyPackage.hb2` `FreyPackage.hp5` `FreyPackage.ha4` `FreyPackage.pp`
`Δ` 📖	mathematical	—	`FreyPackage.freyCurve` `FreyPackage.a` `FreyPackage.b` `FreyPackage.c` `FreyPackage.p`	—	`FreyPackage.hFLT`
`Δ'inv` 📖	mathematical	—	`FreyPackage.freyCurve` `instIsEllipticRatFreyCurve` `FreyPackage.a` `FreyPackage.b` `FreyPackage.c` `FreyPackage.p`	—	`instIsEllipticRatFreyCurve` `Δ`

FreyPackage

Definitions

Name	Category	Theorems
`a` 📖	CompOp	11 math math: `FreyCurve.b₂`, `hgcdac`, `hFLT`, `FreyCurve.c₄`, `ha4`, `hgcdab`, `FreyCurve.c₄'`, `FreyCurve.Δ`, `FreyCurve.j`, `FreyCurve.Δ'inv`, `FreyCurve.b₄`
`b` 📖	CompOp	11 math math: `FreyCurve.b₂`, `hFLT`, `FreyCurve.c₄`, `hgcdab`, `FreyCurve.c₄'`, `hb2`, `FreyCurve.Δ`, `FreyCurve.j`, `FreyCurve.Δ'inv`, `hgcdbc`, `FreyCurve.b₄`
`c` 📖	CompOp	7 math math: `hgcdac`, `hFLT`, `FreyCurve.c₄'`, `FreyCurve.Δ`, `FreyCurve.j`, `FreyCurve.Δ'inv`, `hgcdbc`
`freyCurve` 📖	CompOp	14 math math: `FreyCurve.b₂`, `FreyCurve.c₄`, `FreyCurve.c₄'`, `FreyCurve.torsion_isHardlyRamified`, `Mazur_Frey`, `FreyCurve.Δ`, `FreyCurve.j_valuation_of_bad_prime`, `Wiles_Frey`, `FreyCurve.j`, `FreyCurve.Δ'inv`, `FreyCurve.instIsEllipticRatFreyCurve`, `FreyCurve.torsion_not_isIrreducible`, `FreyCurve.b₄`, `FreyCurve.map`
`freyCurveInt` 📖	CompOp	1 math math: `FreyCurve.map`
`p` 📖	CompOp	17 math math: `FreyCurve.b₂`, `pp`, `hFLT`, `FreyCurve.c₄`, `hp_odd`, `FreyCurve.c₄'`, `FreyCurve.torsion_isHardlyRamified`, `Mazur_Frey`, `hppos`, `FreyCurve.Δ`, `FreyCurve.j_valuation_of_bad_prime`, `Wiles_Frey`, `FreyCurve.j`, `FreyCurve.Δ'inv`, `hp5`, `FreyCurve.torsion_not_isIrreducible`, `FreyCurve.b₄`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gcdab_eq_gcdac` 📖	—	—	—	—	—
`hFLT` 📖	mathematical	—	`a` `p` `b` `c`	—	—
`ha0` 📖	—	—	—	—	—
`ha4` 📖	mathematical	—	`a`	—	—
`hb0` 📖	—	—	—	—	—
`hb2` 📖	mathematical	—	`b`	—	—
`hc0` 📖	—	—	—	—	—
`hgcdab` 📖	mathematical	—	`a` `b`	—	—
`hgcdac` 📖	mathematical	—	`a` `c`	—	`gcdab_eq_gcdac` `hppos` `hFLT` `hgcdab`
`hgcdbc` 📖	mathematical	—	`b` `c`	—	`gcdab_eq_gcdac` `hppos` `hFLT` `hgcdab`
`hp0` 📖	—	—	—	—	`hppos`
`hp5` 📖	mathematical	—	`p`	—	—
`hp_odd` 📖	mathematical	—	`p`	—	`pp` `hp5`
`hppos` 📖	mathematical	—	`p`	—	`hp5`
`of_not_FermatLastTheorem` 📖	mathematical	—	`FreyPackage`	—	`FermatLastTheorem.of_p_ge_5` `of_not_FermatLastTheorem_p_ge_5`
`of_not_FermatLastTheorem_p_ge_5` 📖	mathematical	—	`FreyPackage`	—	`gcdab_eq_gcdac`
`pp` 📖	mathematical	—	`p`	—	—

PNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_add_pow_ne_pow_of_FermatLastTheorem` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`FreyPackage` 📖	CompData	2 math math: `FreyPackage.of_not_FermatLastTheorem`, `FreyPackage.of_not_FermatLastTheorem_p_ge_5`

---

← Back to Index