Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.formally_etale.iff_unramified_and_smooth

Modification history

2022-07-19 11:15
src/ring_theory/etale.lean
feat(ring_theory/etale): Formally étale morphisms. (#15242)
Added algebra.formally_etale.iff_unramified_and_smoothView on Github →