Theorem isPurelyInseparable_iff_subsingleton_emb

Modification history

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