Two-sided ideal compatibility helpers

This file restores upstream scalar-action helpers for two-sided ideals.

theorem TwoSidedIdeal.smul_mem {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {x : R} (r : R) (hx : x ∈ I) : r • x ∈ I

@[implicit_reducible]

instance TwoSidedIdeal.instModuleMulOppositeSubtypeMemLeanPool {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} : Module Rᵐᵒᵖ ↥I

Equations

• One or more equations did not get rendered due to their size.