no goals
R : Type ?u.903066
M✝ : Type ?u.903069
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module R M✝
R₁ : Type ?u.903105
M₁ : Type ?u.903108
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.903720
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.903907
M₃ : Type ?u.903910
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.904498
K : Type ?u.904501
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B✝ : BilinForm R M✝
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_2
o : Type ?u.905718
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : DecidableEq n
inst✝ : DecidableEq o
B : BilinForm R₂ (n → R₂)
M : Matrix n n R₂
⊢ ↑toMatrix' B ⬝ M = ↑toMatrix' (compRight B (↑Matrix.toLin' M))
simp only [toMatrix'_compRight, toMatrix'_toLin']