no goals
R : Type u_1
R₁ : Type ?u.439810
R₂ : Type ?u.439813
R₃ : Type ?u.439816
M : Type u_2
M₁ : Type ?u.439822
M₂ : Type ?u.439825
Mₗ₁ : Type ?u.439828
Mₗ₁' : Type ?u.439831
Mₗ₂ : Type ?u.439834
Mₗ₂' : Type ?u.439837
K : Type ?u.439840
K₁ : Type ?u.439843
K₂ : Type ?u.439846
V : Type ?u.439849
V₁ : Type ?u.439852
V₂ : Type ?u.439855
n : Type ?u.439858
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B F : M →ₗ[R] M →ₗ[R] R
f : Module.End R M
⊢ (∀ (x y : M), ↑(↑B (↑f x)) y = ↑(↑B x) (↑(-f) y)) ↔ ∀ (x y : M), ↑(↑B (↑f x)) y = ↑(↑(-B) x) (↑f y)
simp