Theorems · Theorem · commutative algebra

LinearMap.toMatrix_baseChange

∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} {ι₂ : Type u_5} (A : Type u_6) [inst : Fintype ι]
  [inst_1 : Finite ι₂] [inst_2 : DecidableEq ι] [inst_3 : CommSemiring R] [inst_4 : CommSemiring A]
  [inst_5 : Algebra R A] [inst_6 : AddCommMonoid M₁] [inst_7 : Module R M₁] [inst_8 : AddCommMonoid M₂]
  [inst_9 : Module R M₂] (f : M₁ →ₗ[R] M₂) (b₁ : Module.Basis ι R M₁) (b₂ : Module.Basis ι₂ R M₂),
  (LinearMap.toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂))
      (LinearMap.baseChange A f) =
    ((LinearMap.toMatrix b₁ b₂) f).map ⇑(algebraMap R A)

Defined in

Mathlib.RingTheory.TensorProduct.Free

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeFiniteDecidableEqCommSemiringCommSemiringAlgebraAddCommMonoidModuleAddCommMonoidModule