Theorems · Theorem · linear algebra

mk_eq_mk_of_basis

• 1000+ list: Dimension theorem for vector spaces

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  {ι' : Type w'} [InvariantBasisNumber R] (v : Module.Basis ι R M) (v' : Module.Basis ι' R M),
  Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')

The dimension theorem: if v and v' are two bases, their index types have the same cardinalities.

Defined in

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleInvariantBasisNumber