R : Type u_1
R₁ : Type ?u.849082
R₂ : Type ?u.849085
M : Type ?u.849088
M₁ : Type ?u.849091
M₂ : Type ?u.849094
M₁' : Type ?u.849097
M₂' : Type ?u.849100
n : Type u_2
m : Type u_3
n' : Type ?u.849109
m' : Type u_4
ι : Type ?u.849115
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
f : (m' → R) →ₗ[R] m → R
⊢ ↑toMatrix₂' (compl₁₂ B id f) = ↑toMatrix₂' (comp B id) ⬝ ↑toMatrix' f
R : Type u_1
R₁ : Type ?u.849082
R₂ : Type ?u.849085
M : Type ?u.849088
M₁ : Type ?u.849091
M₂ : Type ?u.849094
M₁' : Type ?u.849097
M₂' : Type ?u.849100
n : Type u_2
m : Type u_3
n' : Type ?u.849109
m' : Type u_4
ι : Type ?u.849115
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
f : (m' → R) →ₗ[R] m → R
⊢ ↑toMatrix₂' (compl₂ B f) = ↑toMatrix₂' B ⬝ ↑toMatrix' f
rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂]
no goals
R : Type u_1
R₁ : Type ?u.849082
R₂ : Type ?u.849085
M : Type ?u.849088
M₁ : Type ?u.849091
M₂ : Type ?u.849094
M₁' : Type ?u.849097
M₂' : Type ?u.849100
n : Type u_2
m : Type u_3
n' : Type ?u.849109
m' : Type u_4
ι : Type ?u.849115
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
f : (m' → R) →ₗ[R] m → R
⊢ ↑toMatrix₂' (compl₁₂ B id f) = ↑toMatrix₂' (comp B id) ⬝ ↑toMatrix' f
simp