Def TwoSidedIdeal.coeAddMonoidHom

Modification history

2024-07-07 22:12

Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

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

Added TwoSidedIdeal.coeAddMonoidHom View on Github →