Theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux

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_etale_isIdempotentElem_forall_liesOver_eq_auxView on Github →