Theorems · Theorem · commutative algebra

IsBaseChange.endHom_toMatrix

∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α : M →ₗ[R] P} (ibcM : IsBaseChange S α) {ι : Type u_7}
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] (b : Module.Basis ι R M) (f : M →ₗ[R] M),
  (LinearMap.toMatrix (IsBaseChange.basis b ibcM) (IsBaseChange.basis b ibcM)) (ibcM.endHom f) =
    ((LinearMap.toMatrix b b) f).map ⇑(algebraMap R S)

Defined in

Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidModuleAddCommMonoidModuleModuleIsScalarTowerDecidableEqFintype