Theorems · Theorem · linear algebra

Module.Basis.restrictScalars_repr_apply

∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : Ring S] [inst_3 : Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M]
  [inst_7 : Module R M] [inst_8 : IsScalarTower R S M] [inst_9 : Module.IsTorsionFree R S] (b : Module.Basis ι S M)
  (m : ↥(Submodule.span R (Set.range ⇑b))) (i : ι),
  (algebraMap R S) (((Module.Basis.restrictScalars R b).repr m) i) = (b.repr ↑m) i

Defined in

Mathlib.LinearAlgebra.Basis.Submodule

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainRingNontrivialAddCommGroupAlgebraModuleModuleIsScalarTowerModule.IsTorsionFree