Theorems · Inductive type · linear algebra

Module.Basis

Type u_1 →
  (R : Type u_3) →
    (M : Type u_6) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max (max u_1 u_3) u_6)

A Basis ι R M for a module M is the type of ι-indexed R-bases of M. The basis vectors are available as DFunLike.coe (b : Basis ι R M) : ι → M. To turn a linear independent family of vectors spanning M into a basis, use Basis.mk. They are internally represented as linear equivs M ≃ₗ[R] (ι →₀ R), available as Basis.repr.

Defined in

Mathlib.LinearAlgebra.Basis.Defs

Cited by

1,477 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SemiringAddCommMonoidModule