Theorem Algebra.FormallyUnramified.iff_comp_injective

Modification history

2024-10-26 17:00
Mathlib/RingTheory/Unramified/Basic.lean
refactor(RingTheory/Unramified): Switch official definition to allow general universes (#15135) …
Added Algebra.FormallyUnramified.iff_comp_injectiveView on Github →