Theorem Algebra.FormallyUnramified.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.comp_injectiveView on Github →