Documentation Verification Report

Instances

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/Instances.lean

Statistics

Metric	Count
Definitions `instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuationOfValuativeExtension_classFieldTheory`, `instMulSemiringActionSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instSMulSubtypeMemSubringIntegerValueGroupWithZeroValuationOfValuativeExtension_classFieldTheory`	3
Theorems `instIsGaloisGroupSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instSMulCommClassSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `valuation_ringEquiv`	3
Total	6
⚠️ With sorry `instIsGaloisGroupSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `valuation_ringEquiv`	2

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuationOfValuativeExtension_classFieldTheory` 📖	CompOp	1 math math: `instIsGaloisGroupSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`instMulSemiringActionSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	CompOp	2 math math: `instSMulCommClassSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`, `instIsGaloisGroupSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`instSMulSubtypeMemSubringIntegerValueGroupWithZeroValuationOfValuativeExtension_classFieldTheory` 📖	CompOp	1 math math: `instSMulCommClassSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsGaloisGroupSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖 ⚠️	mathematical	—	`instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuationOfValuativeExtension_classFieldTheory` `instMulSemiringActionSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`	—	`instSMulCommClassSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory`
`instSMulCommClassSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` 📖	mathematical	—	`instMulSemiringActionSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory` `instSMulSubtypeMemSubringIntegerValueGroupWithZeroValuationOfValuativeExtension_classFieldTheory`	—	—
`valuation_ringEquiv` 📖 ⚠️	—	—	—	—	—

---

← Back to Index