Defs

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

Statistics

Metric	Count
Definitions IsHardlyRamified, Z2bar, instMulActionAbsoluteGaloisGroupPadicOfNatNatSubtypeAlgebraicClosureMemValuationSubringZ2bar	3
Theorems det, isFlat, isTameAtTwo, isUnramified	4
Total	7

GaloisRepresentation

Definitions

Name	Category	Theorems
IsHardlyRamified 📖	CompData	1 math math: FreyCurve.torsion_isHardlyRamified
Z2bar 📖	CompOp	1 math math: IsHardlyRamified.isTameAtTwo
instMulActionAbsoluteGaloisGroupPadicOfNatNatSubtypeAlgebraicClosureMemValuationSubringZ2bar 📖	CompOp	1 math math: IsHardlyRamified.isTameAtTwo

GaloisRepresentation.IsHardlyRamified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det 📖	mathematical	GaloisRepresentation.IsHardlyRamified	GaloisRep.det	—	—
isFlat 📖	mathematical	GaloisRepresentation.IsHardlyRamified	GaloisRep.IsFlatAt Nat.Prime.toHeightOneSpectrumRingOfIntegersRat	—	—
isTameAtTwo 📖	mathematical	GaloisRepresentation.IsHardlyRamified	GaloisRep instFunLikeGaloisRepAbsoluteGaloisGroupEnd GaloisRep.map GaloisRepresentation.Z2bar GaloisRepresentation.instMulActionAbsoluteGaloisGroupPadicOfNatNatSubtypeAlgebraicClosureMemValuationSubringZ2bar GaloisRep.ker	—	—
isUnramified 📖	mathematical	GaloisRepresentation.IsHardlyRamified	GaloisRep.IsUnramifiedAt Nat.Prime.toHeightOneSpectrumRingOfIntegersRat	—	—

---

← Back to Index