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.
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
.
An ideal is radical if it contains its radical.
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.
Ideal.radical
as an InfTopHom
, bundling in that it distributes over inf
.
Equations
- Ideal.radicalInfTopHom = { toFun := Ideal.radical, map_inf' := ⋯, map_top' := ⋯ }
The reverse inclusion does not hold for e.g. I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}
.
Equations
- Ideal.instIdemCommSemiring = inferInstance
Alias of Ideal.IsPrime.pow_le_iff
.
Alias of Ideal.IsPrime.le_of_pow_le
.
Alias of Ideal.IsPrime.prod_le
.
The product of a finite number of elements in the commutative semiring R
lies in the
prime ideal p
if and only if at least one of those elements is in p
.
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)
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯