Commit 2024-07-07 22:12 e92b4c2d

View on Github →

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

Estimated changes

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

added def TwoSidedIdeal.coeAddMonoidHom

added theorem TwoSidedIdeal.coe_mop_smul

added theorem TwoSidedIdeal.coe_smul

added def TwoSidedIdeal.subtype

added def TwoSidedIdeal.subtypeMop