Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.formally_smooth.of_equiv

Modification history

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