Pi

Statistics

Metric	Count
Definitions	0
Theorems `instForallOfFinite`, `pi_iff`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instForallOfFinite` 📖	mathematical	`Algebra.FormallyEtale`	`Pi.commRing` `Pi.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`of_formallyUnramified_and_formallySmooth` `Algebra.FormallyUnramified.instForall` `instFormallyUnramified` `Algebra.FormallySmooth.instForallOfFinite` `instFormallySmooth`
`pi_iff` 📖	mathematical	—	`Algebra.FormallyEtale` `Pi.commRing` `Pi.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`Algebra.FormallyUnramified.pi_iff` `Algebra.FormallySmooth.pi_iff`

---