Automorphic

📁 Source: FLT/GaloisRepresentation/Automorphic.lean

Statistics

Metric	Count
Definitions IsAutomorphicOfLevel, instNormedSpacePadicPadicAlgCl_fLT	2
Theorems cyclic_base_change, instContinuousSMulPadicIntAlgebraicClosurePadic_fLT, instIsQuaternionAlgebraTensorProduct	3
Total	5
⚠️ With sorry cyclic_base_change, instIsQuaternionAlgebraTensorProduct	2

GaloisRep

Definitions

Name	Category	Theorems
IsAutomorphicOfLevel 📖	MathDef	1 math math: cyclic_base_change

(root)

Definitions

Name	Category	Theorems
instNormedSpacePadicPadicAlgCl_fLT 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclic_base_change 📖 ⚠️	mathematical	GaloisRep.det GaloisRep.conj GaloisRep.baseChange GaloisRep.IsFlatAt GaloisRep.IsUnramifiedAt localTameAbelianInertiaGroup GaloisRep.ker GaloisRep instFunLikeGaloisRepAbsoluteGaloisGroupEnd GaloisRep.toLocal	GaloisRep.IsAutomorphicOfLevel instContinuousSMulPadicIntAlgebraicClosurePadic_fLT GaloisRep.map IsDedekindDomain.HeightOneSpectrum.preimageComapFinset	—	instContinuousSMulPadicIntAlgebraicClosurePadic_fLT
instContinuousSMulPadicIntAlgebraicClosurePadic_fLT 📖	—	—	—	—	—
instIsQuaternionAlgebraTensorProduct 📖 ⚠️	mathematical	—	IsQuaternionAlgebra	—	—

---

← Back to Index