Theorem RingHom.IsPurelyInseparable.comp

Modification history

2026-06-09 19:37
Mathlib/RingTheory/RingHom/PurelyInseparable.lean
feat(AlgebraicGeometry/Morphisms/UniversallyInjective): equivalent criteria for universally injective morphisms (#39910) …
Added RingHom.IsPurelyInseparable.compView on Github →