Theorems · Definition · linear algebra

Module.Basis.reindexRange

{ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → (b : Module.Basis ι R M) → Module.Basis (↑(Set.range ⇑b)) R M

b.reindexRange is a basis indexed by range b, the basis vectors themselves.

Defined in: Mathlib.LinearAlgebra.Basis.Defs
Cited by: 16 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

DFunLike.coestatement and proof · cited by 62,936
Modulestatement and proof · cited by 20,661
Semiringstatement and proof · cited by 13,802
AddCommMonoidstatement and proof · cited by 12,281
Set.Elemstatement and proof · cited by 7,166
Set.rangestatement and proof · cited by 4,705
Nontrivialproof · cited by 2,416
Module.Basisstatement and proof · cited by 1,477
Equiv.ofInjectiveproof · cited by 64
Module.Basis.reindexproof · cited by 57
Module.Basis.injectiveproof · cited by 11
Module.subsingletonEquivproof · cited by 4

Cited by17

Results whose statement or proof uses this declaration.

Module.Basis.mk_eq_rank''proof · cited by 23
Module.Free.of_basisproof · cited by 20
Module.Basis.reindexFinsetRangeproof · cited by 7
Module.Basis.reindexRange_selfstatement · cited by 4
Module.free_defproof · cited by 3
Module.Free.exists_setproof · cited by 3
Module.Basis.reindexRange_applystatement · cited by 3
Module.Basis.reindexRange_reprstatement · cited by 3
Module.Basis.mk_range_eq_rankproof · cited by 2
Module.Basis.reindexRange_repr_selfstatement and proof · cited by 2
Module.Basis.reindexFinsetRange_selfproof · cited by 1
Module.Basis.reindexRange_repr'statement and proof · cited by 1