Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.formally_smooth.mk_lift

Modification history

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