Theorem IsSimpleRing.injective_ringHom

Modification history

2024-11-14 06:25

Mathlib/RingTheory/SimpleRing/Basic.lean

refactor(RingHom.injective): use simple ring (#18868)

Deleted IsSimpleRing.injective_ringHom View on Github →

2024-11-08 19:01

Mathlib/RingTheory/SimpleRing/Basic.lean

feat(RingTheory/SimpleRing/Basic): characterise simple ring in terms of injectiveness (#18113)

Added IsSimpleRing.injective_ringHom View on Github →