Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.formally_smooth.comp

Modification history

2022-07-19 11:15

src/ring_theory/etale.lean

feat(ring_theory/etale): Formally étale morphisms. (#15242)

Added algebra.formally_smooth.comp View on Github →