Pi

Statistics

Metric	Count
Definitions	0
Theorems `instEtaleForallOfFinite`, `instForallOfFinite`, `pi_iff`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`instEtaleForallOfFinite` 📖	mathematical	`Algebra.Etale`	`Algebra.Etale` `Pi.commRing` `Pi.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`instForallOfFinite` `Algebra.Etale.formallyEtale` `Algebra.FinitePresentation.pi` `Algebra.Etale.finitePresentation`
`instForallOfFinite` 📖	mathematical	`Algebra.FormallyEtale`	`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`

---