R : Type u_1
R₁ : Type ?u.455798
R₂ : Type ?u.455801
R₃ : Type ?u.455804
M : Type u_2
M₁ : Type ?u.455810
M₂ : Type ?u.455813
Mₗ₁ : Type ?u.455816
Mₗ₁' : Type ?u.455819
Mₗ₂ : Type ?u.455822
Mₗ₂' : Type ?u.455825
K : Type ?u.455828
K₁ : Type ?u.455831
K₂ : Type ?u.455834
V : Type ?u.455837
V₁ : Type ?u.455840
V₂ : Type ?u.455843
n : Type ?u.455846
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
⊢ f ∈ skewAdjointSubmodule B ↔ IsAdjointPair (-B) B f f
R : Type u_1
R₁ : Type ?u.455798
R₂ : Type ?u.455801
R₃ : Type ?u.455804
M : Type u_2
M₁ : Type ?u.455810
M₂ : Type ?u.455813
Mₗ₁ : Type ?u.455816
Mₗ₁' : Type ?u.455819
Mₗ₂ : Type ?u.455822
Mₗ₂' : Type ?u.455825
K : Type ?u.455828
K₁ : Type ?u.455831
K₂ : Type ?u.455834
V : Type ?u.455837
V₁ : Type ?u.455840
V₂ : Type ?u.455843
n : Type ?u.455846
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
⊢ f ∈ skewAdjointSubmodule B ↔ IsSkewAdjoint B f
rw [isSkewAdjoint_iff_neg_self_adjoint]
no goals
R : Type u_1
R₁ : Type ?u.455798
R₂ : Type ?u.455801
R₃ : Type ?u.455804
M : Type u_2
M₁ : Type ?u.455810
M₂ : Type ?u.455813
Mₗ₁ : Type ?u.455816
Mₗ₁' : Type ?u.455819
Mₗ₂ : Type ?u.455822
Mₗ₂' : Type ?u.455825
K : Type ?u.455828
K₁ : Type ?u.455831
K₂ : Type ?u.455834
V : Type ?u.455837
V₁ : Type ?u.455840
V₂ : Type ?u.455843
n : Type ?u.455846
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
⊢ f ∈ skewAdjointSubmodule B ↔ IsAdjointPair (-B) B f f
exact Iff.rfl