Theorem Algebra.mem_etaleLocus_iff

Modification history

2025-12-12 15:51

Mathlib/RingTheory/Etale/Locus.lean

feat(RingTheory): the etale locus of an algebra (#32529)

Added Algebra.mem_etaleLocus_iff View on Github →