Documentation
Mathlib
.
RingTheory
.
TwoSidedIdeal
.
Instances
Search
return to top
source
Imports
Init
Mathlib.Algebra.Ring.Defs
Mathlib.RingTheory.NonUnitalSubring.Defs
Mathlib.RingTheory.TwoSidedIdeal.Basic
Imported by
instNonUnitalSubringClassTwoSidedIdeal
Additional instances for two-sided ideals.
#
source
instance
instNonUnitalSubringClassTwoSidedIdeal
{
R
:
Type
u_1}
[
NonUnitalNonAssocRing
R
]
:
NonUnitalSubringClass
(
TwoSidedIdeal
R
)
R