Theorem Algebra.basicOpen_subset_etaleLocus_iff_etale

Modification history

2025-12-12 15:51
Mathlib/RingTheory/Etale/Locus.lean
feat(RingTheory): the etale locus of an algebra (#32529)
Added Algebra.basicOpen_subset_etaleLocus_iff_etaleView on Github →