Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.formally_smooth.of_is_localization

Modification history

2022-08-16 04:11

src/ring_theory/etale.lean

feat(ring_theory/etale): Localization and formally etale homomorphisms. (#15813)

Added algebra.formally_smooth.of_is_localization View on Github →