no goals
R : Type ?u.1220676
M : Type ?u.1220679
inst✝²⁴ : Semiring R
inst✝²³ : AddCommMonoid M
inst✝²² : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝²¹ : Ring R₁
inst✝²⁰ : AddCommGroup M₁
inst✝¹⁹ : Module R₁ M₁
R₂ : Type ?u.1221327
M₂ : Type ?u.1221330
inst✝¹⁸ : CommSemiring R₂
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : Module R₂ M₂
R₃ : Type ?u.1221517
M₃ : Type ?u.1221520
inst✝¹⁵ : CommRing R₃
inst✝¹⁴ : AddCommGroup M₃
inst✝¹³ : Module R₃ M₃
V : Type ?u.1222108
K : Type ?u.1222111
inst✝¹² : Field K
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1223325
M₂'' : Type ?u.1223328
inst✝⁹ : AddCommMonoid M₂'
inst✝⁸ : AddCommMonoid M₂''
inst✝⁷ : Module R₂ M₂'
inst✝⁶ : Module R₂ M₂''
F : BilinForm R M
M' : Type ?u.1223639
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
B' : BilinForm R M'
f✝ f' : M →ₗ[R] M'
g g' : M' →ₗ[R] M
M₁' : Type ?u.1224076
inst✝³ : AddCommGroup M₁'
inst✝² : Module R₁ M₁'
B₁' : BilinForm R₁ M₁'
f₁ f₁' : M₁ →ₗ[R₁] M₁'
g₁ g₁' : M₁' →ₗ[R₁] M₁
B₂' : BilinForm R₂ M₂'
f₂ f₂' : M₂ →ₗ[R₂] M₂'
g₂ g₂' : M₂' →ₗ[R₂] M₂
M'' : Type ?u.1226555
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
B'' : BilinForm R M''
F₂ : BilinForm R₂ M₂
f : Module.End R₁ M₁
⊢ (∀ (x y : M₁), bilin B₁ (↑f x) y = bilin B₁ x (↑(-f) y)) ↔ ∀ (x y : M₁), bilin B₁ (↑f x) y = bilin (-B₁) x (↑f y)
simp only [LinearMap.neg_apply, BilinForm.neg_apply, BilinForm.neg_right]