no goals
R : Type u_1
R₁ : Type ?u.928393
R₂ : Type ?u.928396
M✝ : Type ?u.928399
M₁ : Type ?u.928402
M₂ : Type ?u.928405
M₁' : Type ?u.928408
M₂' : Type ?u.928411
n : Type u_2
m : Type u_3
n' : Type u_4
m' : Type u_5
ι : Type ?u.928426
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix n' n R
N : Matrix m m' R
⊢ M ⬝ ↑toMatrix₂' B ⬝ N = ↑toMatrix₂' (compl₁₂ B (↑toLin' Mᵀ) (↑toLin' N))
simp