Frobenius

📁 Source: FLT/Deformations/RepresentationTheory/Frobenius.lean

Statistics

Metric	Count
Definitions arithFrobAt'	1
Theorems arithFrobAt', exists_of_isInvariant_of_profinite, exists_primesOver_isConj_of_profinite, isConj_arithFrobAt'	4
Total	5

IsArithFrobAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arithFrobAt' 📖	mathematical	—	arithFrobAt'	—	exists_primesOver_isConj_of_profinite
exists_of_isInvariant_of_profinite 📖	—	—	—	—	instContinuousSMulOfDiscreteTopologyOfContinuousSMulDiscrete
exists_primesOver_isConj_of_profinite 📖	—	—	—	—	instContinuousSMulOfDiscreteTopologyOfContinuousSMulDiscrete exists_of_isInvariant_of_profinite

(root)

Definitions

Name	Category	Theorems
arithFrobAt' 📖	CompOp	2 math math: isConj_arithFrobAt', IsArithFrobAt.arithFrobAt'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConj_arithFrobAt' 📖	mathematical	—	arithFrobAt'	—	IsArithFrobAt.exists_primesOver_isConj_of_profinite

---

← Back to Index