Theorem RingHom.IsPurelyInseparable.containsIdentities

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.containsIdentitiesView on Github →