Theorems · Definition · linear algebra

Submodule.IsPrincipal.generator

{R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (S : Submodule R M) → [S.IsPrincipal] → M

generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I

Defined in

Mathlib.LinearAlgebra.Span.Defs

Cited by

56 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleSubmodule.IsPrincipal