Theorems · Definition · linear algebra

Module.finBasisOfFinrankEq

(R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [Module.Free R M] →
            [StrongRankCondition R] → [Module.Finite R M] → {n : ℕ} → Module.finrank R M = n → Module.Basis (Fin n) R M

A rank n free module has a basis indexed by Fin n.

Defined in: Mathlib.LinearAlgebra.Dimension.Free
Cited by: 6 results in Mathlib
Foundations: Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring AddCommMonoid Module Module.Free StrongRankCondition Module.Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
Semiringstatement and proof · cited by 13,802
AddCommMonoidstatement and proof · cited by 12,281
Module.finrankstatement and proof · cited by 1,770
Module.Basisstatement · cited by 1,477
Module.Finitestatement and proof · cited by 1,032
Module.Freestatement and proof · cited by 597
StrongRankConditionstatement and proof · cited by 286
finCongrproof · cited by 78
Module.Basis.reindexproof · cited by 57
Module.finBasisproof · cited by 22

Cited by7

Results whose statement or proof uses this declaration.

Module.basisUniqueproof · cited by 5
Module.nonempty_basis_of_flat_of_finrank_eqproof · cited by 1
Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradiusproof · cited by 1
AlternatingMap.measure_defstatement and proof · cited by 1
AlternatingMap.measure_parallelepipedproof · cited by 1
EuclideanGeometry.cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_piproof · cited by 0
Module.finBasisOfFinrankEq.congr_simpstatement and proof · cited by 0