Def TwoSidedIdeal.subtypeMop

Modification history

2024-11-14 06:25

Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

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

Modified TwoSidedIdeal.subtypeMop View on Github →

2024-07-07 22:12

Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

feat(RingTheory/TwoSidedIdeal/Basic): two-sided-ideal as a bimodule (#14453)

Added TwoSidedIdeal.subtypeMop View on Github →