Fermat's Last Theorem in Lean 4

← all areas

Namespace CerednikDrinfeld 2,376 theorems

237 · BruhatTits 17 · CSTower 5 · CartierLift 1 · CosetGraph 40 · EdgeFamily 3 · FormalODModule 225 · FormalOmega 222 · FormalQuotientDatum 2 · GradedCartierModuleData 49 · HeckeTower 5 · JPrimeTorsionDatum 2 · LevelU 3 · Mumford 50 · Omega 178 · OmegaNr 1 · Onr 3 · QM 1063 · ShimuraCurveModel 10 · SpecialFormal 197 · SpecialFormalODModule 54 · SpecialModule 3 · TwoPlaceTorsionDatum 3 · UnramQuad 3

directly in CerednikDrinfeld 237

CerednikDrinfeld.BruhatTits 17

CerednikDrinfeld.CSTower 5

CerednikDrinfeld.CartierLift 1

CerednikDrinfeld.CosetGraph 40

CerednikDrinfeld.EdgeFamily 3

CerednikDrinfeld.FormalODModule 225

CerednikDrinfeld.FormalOmega 222

CerednikDrinfeld.FormalQuotientDatum 2

CerednikDrinfeld.GradedCartierModuleData 49

CerednikDrinfeld.HeckeTower 5

CerednikDrinfeld.JPrimeTorsionDatum 2

CerednikDrinfeld.LevelU 3

CerednikDrinfeld.Mumford 50

CerednikDrinfeld.Omega 178

CerednikDrinfeld.OmegaNr 1

CerednikDrinfeld.Onr 3

CerednikDrinfeld.QM 1063

CerednikDrinfeld.ShimuraCurveModel 10

CerednikDrinfeld.SpecialFormal 197

CerednikDrinfeld.SpecialFormalODModule 54

CerednikDrinfeld.SpecialModule 3

CerednikDrinfeld.TwoPlaceTorsionDatum 3

CerednikDrinfeld.UnramQuad 3