Theorem Algebra.FormallyUnramified.of_surjective

Modification history

2024-10-03 17:44

Mathlib/RingTheory/Unramified/Basic.lean

feat(RingTheory/Unramified): Formally unramified product of rings (#15141)

Added Algebra.FormallyUnramified.of_surjective View on Github →