Theorems · Theorem · commutative algebra

Module.free_def

∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{w, v} M],
  Module.Free R M ↔ ∃ I, Nonempty (Module.Basis I R M)

If M fits in universe w, then freeness is equivalent to existence of a basis in that universe. Note that if M does not fit in w, the reverse direction of this implication is still true as Module.Free.of_basis.

Defined in

Mathlib.LinearAlgebra.FreeModule.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleSmall