More operations on modules and ideals #
Equations
- Submodule.hasSMul' = { smul := Submodule.map₂ (LinearMap.lsmul R M) }
This duplicates the global smul_eq_mul
, but doesn't have to unfold anywhere near as much to
apply.
Module.annihilator R M
is the ideal of all elements r : R
such that r • M = 0
.
Equations
- Module.annihilator R M = LinearMap.ker (LinearMap.lsmul R M)
Instances For
N.annihilator
is the ideal of all elements r : R
such that r • N = 0
.
Equations
- N.annihilator = Module.annihilator R ↥N
Instances For
Dependent version of Submodule.smul_induction_on
.
Equations
- ⋯ = ⋯
Given s
, a generating set of R
, to check that an x : M
falls in a
submodule M'
of x
, we only need to show that r ^ n • x ∈ M'
for some n
for each r : s
.
If x
is an I
-multiple of the submodule spanned by f '' s
,
then we can write x
as an I
-linear combination of the elements of f '' s
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Alias of Ideal.inf_eq_mul_of_isCoprime
.
The radical of an ideal I
consists of the elements r
such that r ^ n ∈ I
for some n
.
Equations
Instances For
An ideal is radical if it contains its radical.
Instances For
An ideal is radical iff it is equal to its radical.
Alias of the reverse direction of Ideal.radical_eq_iff
.
An ideal is radical iff it is equal to its radical.
The reverse inclusion does not hold for e.g. I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}
.
Equations
- Ideal.instIdemCommSemiring = inferInstance
If I
divides J
, then I
contains J
.
In a Dedekind domain, to divide and contain are equivalent, see Ideal.dvd_iff_le
.
Equations
- Ideal.uniqueUnits = { default := 1, uniq := ⋯ }
A variant of Finsupp.linearCombination
that takes in vectors valued in I
.
Equations
- Ideal.finsuppTotal ι M I v = Finsupp.linearCombination R v ∘ₗ Finsupp.mapRange.linearMap (Submodule.subtype I)
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯