Theorem Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocus

Modification history

2026-09-26 18:40
Mathlib/RingTheory/Etale/Locus.lean
chore: fix misspellings in declaration names (#44049) …
Deleted Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocusView on Github →
2025-12-12 15:51
Mathlib/RingTheory/Etale/Locus.lean
feat(RingTheory): the etale locus of an algebra (#32529)
Added Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocusView on Github →