Theorems · Theorem · linear algebra

Module.Basis.restrictScalars_toMatrix

∀ {ι : Type u_1} (R₂ : Type u_7) {M₂ : Type u_8} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] {S : Type u_9} [inst_5 : CommRing S] [inst_6 : Nontrivial S]
  [inst_7 : Algebra R₂ S] [inst_8 : Module S M₂] [inst_9 : IsScalarTower R₂ S M₂] [inst_10 : IsDomain R₂]
  [inst_11 : Module.IsTorsionFree R₂ S] (b : Module.Basis ι S M₂) (v : ι → ↥(Submodule.span R₂ (Set.range ⇑b))),
  (algebraMap R₂ S).mapMatrix ((Module.Basis.restrictScalars R₂ b).toMatrix v) = b.toMatrix fun i => ↑(v i)

Defined in

Mathlib.LinearAlgebra.Matrix.Basis

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleFintypeDecidableEqCommRingNontrivialAlgebraModuleIsScalarTowerIsDomainModule.IsTorsionFree