Documentation Verification Report

AdicTopology

📁 Source: FLT/Patching/Utils/AdicTopology.lean

Statistics

Metric	Count
Definitions `IsAdicTopology`, `withIdeal`	2
Theorems `of_isLocalHom`, `isCompact_of_fg`, `isAdic`, `compactSpace`, `isCompact_of_fg`, `compactSpace_of_finite_residueField`, `hasBasis_maximalIdeal_pow`, `instDiscreteTopologyOfIsArtinianRing_fLT`, `instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT`, `instIsAdicTopology`, `instIsAdicTopologyOfIsNoetherianRingOfCompactSpaceOfT2SpaceOfTotallyDisconnectedSpace`, `instIsHausdorffMaximalIdealOfIsNoetherianRing_fLT`, `instIsLinearTopology_fLT`, `instIsPrecompleteMaximalIdealOfCompactSpace_fLT`, `instNonarchimedeanRing_fLT`, `instT2SpaceOfIsNoetherianRing_fLT`, `isCompact_of_isNoetherianRing`, `isOpen_iff_finite_quotient'`, `isOpen_maximalIdeal'`, `isOpen_maximalIdeal_pow'`, `isOpen_maximalIdeal_pow''`	21
Total	23

IsLocalRing

Definitions

Name	Category	Theorems
`IsAdicTopology` 📖	CompData	3 math math: `Deformation.ProartinianCat.instIsAdicTopologyCarrierSelf`, `instIsAdicTopologyOfIsNoetherianRingOfCompactSpaceOfT2SpaceOfTotallyDisconnectedSpace`, `instIsAdicTopology`
`withIdeal` 📖	CompOp	1 math math: `instIsAdicTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_of_finite_residueField` 📖	—	—	—	—	`instNonarchimedeanRing_fLT` `hasBasis_maximalIdeal_pow` `instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT`
`hasBasis_maximalIdeal_pow` 📖	—	—	—	—	`IsAdicTopology.isAdic`
`instDiscreteTopologyOfIsArtinianRing_fLT` 📖	—	—	—	—	`isOpen_maximalIdeal_pow''`
`instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT` 📖	—	—	—	—	`isOpen_maximalIdeal_pow''`
`instIsAdicTopology` 📖	mathematical	—	`IsAdicTopology` `withIdeal`	—	—
`instIsAdicTopologyOfIsNoetherianRingOfCompactSpaceOfT2SpaceOfTotallyDisconnectedSpace` 📖	mathematical	—	`IsAdicTopology`	—	`isOpen_maximalIdeal_pow'` `exists_ideal_isOpen_and_subset`
`instIsHausdorffMaximalIdealOfIsNoetherianRing_fLT` 📖	—	—	—	—	—
`instIsLinearTopology_fLT` 📖	—	—	—	—	`hasBasis_maximalIdeal_pow`
`instIsPrecompleteMaximalIdealOfCompactSpace_fLT` 📖	—	—	—	—	`instDiscreteTopologyQuotientIdealHPowNatMaximalIdeal_fLT` `denseRange_inverseLimit` `instNonarchimedeanRing_fLT`
`instNonarchimedeanRing_fLT` 📖	—	—	—	—	`IsAdicTopology.isAdic`
`instT2SpaceOfIsNoetherianRing_fLT` 📖	—	—	—	—	`instNonarchimedeanRing_fLT` `isOpen_maximalIdeal_pow''`
`isCompact_of_isNoetherianRing` 📖	—	—	—	—	`Ideal.isCompact_of_fg`
`isOpen_iff_finite_quotient'` 📖	—	—	—	—	`isOpen_maximalIdeal_pow''`
`isOpen_maximalIdeal'` 📖	—	—	—	—	`isOpen_maximalIdeal_pow''`
`isOpen_maximalIdeal_pow'` 📖	—	—	—	—	`isCompact_of_isNoetherianRing`
`isOpen_maximalIdeal_pow''` 📖	—	—	—	—	`IsAdicTopology.isAdic`

IsLocalRing.Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isLocalHom` 📖	—	—	—	—	`IsLocalRing.instNonarchimedeanRing_fLT` `IsLocalRing.hasBasis_maximalIdeal_pow`

IsLocalRing.Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_of_fg` 📖	—	—	—	—	`IsLocalRing.Submodule.isCompact_of_fg`

IsLocalRing.IsAdicTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAdic` 📖	—	—	—	—	—

IsLocalRing.IsModuleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace` 📖	—	—	—	—	`IsLocalRing.Submodule.isCompact_of_fg`

IsLocalRing.Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_of_fg` 📖	—	—	—	—	—

---

← Back to Index