Theorem Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver

Modification history

2026-02-10 18:25
Mathlib/RingTheory/Etale/QuasiFinite.lean
feat(RingTheory): etale local structure of quasi-finite algebras (#35036)
Added Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOverView on Github →