Change of basis for comodule coefficient matrices

The coefficient matrices of a finite free comodule intertwine with the scalar extension of the change-of-basis matrix. This turns a triangular comodule basis into a conjugation of the corresponding matrix-valued point.

theorem Module.Basis.coefficientMatrix_mul_toMatrix {R : Type u_1} {C : Type u_2} {M : Type u_3} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] [Fintype ι] [Fintype κ] (b : Basis ι R M) (c : Basis κ R M) : TauCeti.Comodule.coefficientMatrix b * (b.toMatrix ⇑c).map ⇑(algebraMap R C) = (b.toMatrix ⇑c).map ⇑(algebraMap R C) * TauCeti.Comodule.coefficientMatrix c

Coefficient matrices intertwine with the change-of-basis matrix, extended to the coefficient algebra. The bases may have different finite index types.