Theorems · Definition · commutative algebra

Submodule.spanRank

{R : Type u_1} →
  {M : Type u} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Cardinal.{u}

The minimum cardinality of a generating set of a submodule as a cardinal.

Defined in

Mathlib.Algebra.Module.SpanRank

Cited by

61 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule