Documentation
Atlas
.
LieGroups
.
code
.
PrimitiveIdeal
Search
return to top
source
Imports
Init
Mathlib.RingTheory.SimpleModule.Basic
Mathlib.RingTheory.TwoSidedIdeal.Basic
Imported by
TwoSidedIdeal
.
moduleAnnihilator
TwoSidedIdeal
.
IsPrimitive
source
def
TwoSidedIdeal
.
moduleAnnihilator
(
R
:
Type
u_2)
[
Ring
R
]
(
M
:
Type
u_3)
[
AddCommGroup
M
]
[
Module
R
M
]
:
TwoSidedIdeal
R
Instances For
source
def
TwoSidedIdeal
.
IsPrimitive
{
R
:
Type
u_1}
[
Ring
R
]
(
I
:
TwoSidedIdeal
R
)
:
Prop
Instances For