Documentation
Mathlib
.
RingTheory
.
TwoSidedIdeal
.
Instances
Search
Google site 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
Equations
⋯
=
⋯