Theorems · Definition · commutative algebra

Module.eqIdeal

(R : Type u_1) → {M : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → M → M → Ideal R

For two elements m and m' in an R-module M, the set of elements r : R with equal scalar product with m and m' is an ideal of R. If M is a group, this coincides with the kernel of LinearMap.toSpanSingleton R M (m - m').

Defined in

Mathlib.RingTheory.Ideal.Defs

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

SemiringAddCommMonoidModule