Theorem TwoSidedIdeal.coe_mop_smul

Modification history

2024-11-14 06:25
Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
refactor(RingHom.injective): use simple ring (#18868)
Modified TwoSidedIdeal.coe_mop_smulView 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.coe_mop_smulView on Github →