Theorem Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt.{u,

Modification history

2026-02-13 17:17
Mathlib/RingTheory/ZariskisMainTheorem.lean
feat(RingTheory): weakly quasi finite primes (#35234)
Added Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt.{u,View on Github →