Theorem RingHom.isPurelyInseparable_algebraMap_iff

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_algebraMap_iffView on Github →