Documentation Verification Report

IsProartinian

📁 Source: FLT/Deformations/IsProartinian.lean

Statistics

Metric	Count
Definitions `IsProartinian`	1
Theorems `isArtinianRing_quotient`, `toCompleteSpace`, `toIsLinearTopology`, `toT0Space`, `exists_maximalIdeal_pow_le_of_isProartinian`, `instIsProartinianOfDiscreteTopologyOfIsArtinianRing`, `instIsProartinianOfIsAdicTopologyOfIsNoetherianRingOfCompactSpace`, `isContinuous_of_isProartinian_of_isLocalHom`, `isLocalHom_of_isContinuous_of_isProartinian`, `isOpen_maximalIdeal_of_isProartinian`, `isProartinian_iff_isArtinianRing`	11
Total	12

IsProartinian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArtinianRing_quotient` 📖	—	—	—	—	—
`toCompleteSpace` 📖	—	—	—	—	—
`toIsLinearTopology` 📖	—	—	—	—	—
`toT0Space` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`IsProartinian` 📖	CompData	4 math math: `instIsProartinianOfDiscreteTopologyOfIsArtinianRing`, `isProartinian_iff_isArtinianRing`, `Deformation.IsLocalProartinianAlgebra.toIsProartinian`, `instIsProartinianOfIsAdicTopologyOfIsNoetherianRingOfCompactSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_maximalIdeal_pow_le_of_isProartinian` 📖	—	—	—	—	`IsProartinian.isArtinianRing_quotient` `IsLocalRing.map_maximalIdeal`
`instIsProartinianOfDiscreteTopologyOfIsArtinianRing` 📖	mathematical	—	`IsProartinian`	—	`isProartinian_iff_isArtinianRing`
`instIsProartinianOfIsAdicTopologyOfIsNoetherianRingOfCompactSpace` 📖	mathematical	—	`IsProartinian`	—	`IsLocalRing.instIsLinearTopology_fLT` `IsLocalRing.instT2SpaceOfIsNoetherianRing_fLT` `IsLocalRing.instNonarchimedeanRing_fLT`
`isContinuous_of_isProartinian_of_isLocalHom` 📖	—	—	—	—	`IsLocalRing.instNonarchimedeanRing_fLT` `IsLocalRing.hasBasis_maximalIdeal_pow` `IsProartinian.toIsLinearTopology` `exists_maximalIdeal_pow_le_of_isProartinian`
`isLocalHom_of_isContinuous_of_isProartinian` 📖	—	—	—	—	`exists_maximalIdeal_pow_le_of_isProartinian` `isOpen_maximalIdeal_of_isProartinian`
`isOpen_maximalIdeal_of_isProartinian` 📖	—	—	—	—	`IsLinearTopology.exists_ideal_isMaximal_and_isOpen` `IsProartinian.toIsLinearTopology` `IsProartinian.toT0Space`
`isProartinian_iff_isArtinianRing` 📖	mathematical	—	`IsProartinian`	—	`IsProartinian.isArtinianRing_quotient` `IsTopologicalAddGroup.discreteUniformity`

---

← Back to Index