Theorem Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq

Modification history

2026-01-06 11:03
Mathlib/RingTheory/Etale/QuasiFinite.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added Algebra.exists_etale_isIdempotentElem_forall_liesOver_eqView on Github →