refactor: make LinearMap.IsAdjointPair accept bare functions as arg…

…uments (#19679)

Co-authored-by: Oliver Nash <[email protected]>

Mathlib/Algebra/Lie/SkewAdjoint.lean

@@ -45,8 +45,8 @@ theorem LinearMap.BilinForm.isSkewAdjoint_bracket {f g : Module.End R M}
     (hf : f ∈ B.skewAdjointSubmodule) (hg : g ∈ B.skewAdjointSubmodule) :
     ⁅f, g⁆ ∈ B.skewAdjointSubmodule := by
   rw [mem_skewAdjointSubmodule] at *
-  have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hf.mul hg
-  have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hg.mul hf
+  have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hg.comp hf
+  have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hf.comp hg
   change IsAdjointPair B B (f * g - g * f) (-(f * g - g * f)); rw [neg_sub]
   exact hfg.sub hgf
 
@@ -61,7 +61,7 @@ variable {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M)
 /-- An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint
 endomorphisms. -/
 def skewAdjointLieSubalgebraEquiv :
-    skewAdjointLieSubalgebra (B.compl₁₂ (↑e : N →ₗ[R] M) ↑e) ≃ₗ⁅R⁆ skewAdjointLieSubalgebra B := by
+    skewAdjointLieSubalgebra (B.compl₁₂ (e : N →ₗ[R] M) e) ≃ₗ⁅R⁆ skewAdjointLieSubalgebra B := by
   apply LieEquiv.ofSubalgebras _ _ e.lieConj
   ext f
   simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule,

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -154,140 +154,6 @@ theorem isAlt_zero : (0 : BilinForm R M).IsAlt := fun _ => rfl
 theorem isAlt_neg {B : BilinForm R₁ M₁} : (-B).IsAlt ↔ B.IsAlt :=
   ⟨fun h => neg_neg B ▸ h.neg, IsAlt.neg⟩
 
-/-! ### Linear adjoints -/
-
-
-section LinearAdjoints
-
-variable (B) (F : BilinForm R M)
-variable {M' : Type*} [AddCommMonoid M'] [Module R M']
-variable (B' : BilinForm R M') (f f' : M →ₗ[R] M') (g g' : M' →ₗ[R] M)
-
-/-- Given a pair of modules equipped with bilinear forms, this is the condition for a pair of
-maps between them to be mutually adjoint. -/
-def IsAdjointPair :=
-  ∀ ⦃x y⦄, B' (f x) y = B x (g y)
-
-variable {B B' f f' g g'}
-
-theorem IsAdjointPair.eq (h : IsAdjointPair B B' f g) : ∀ {x y}, B' (f x) y = B x (g y) :=
-  @h
-
-theorem isAdjointPair_iff_compLeft_eq_compRight (f g : Module.End R M) :
-    IsAdjointPair B F f g ↔ F.compLeft f = B.compRight g := by
-  constructor <;> intro h
-  · ext x
-    simp only [compLeft_apply, compRight_apply]
-    apply h
-  · intro x y
-    rw [← compLeft_apply, ← compRight_apply]
-    rw [h]
-
-theorem isAdjointPair_zero : IsAdjointPair B B' 0 0 := fun x y => by
-  simp only [BilinForm.zero_left, BilinForm.zero_right, LinearMap.zero_apply]
-
-theorem isAdjointPair_id : IsAdjointPair B B 1 1 := fun _ _ => rfl
-
-theorem IsAdjointPair.add (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') :
-    IsAdjointPair B B' (f + f') (g + g') := fun x y => by
-  rw [LinearMap.add_apply, LinearMap.add_apply, add_left, add_right, h, h']
-
-variable {M₁' : Type*} [AddCommGroup M₁'] [Module R₁ M₁']
-variable {B₁' : BilinForm R₁ M₁'} {f₁ f₁' : M₁ →ₗ[R₁] M₁'} {g₁ g₁' : M₁' →ₗ[R₁] M₁}
-
-theorem IsAdjointPair.sub (h : IsAdjointPair B₁ B₁' f₁ g₁) (h' : IsAdjointPair B₁ B₁' f₁' g₁') :
-    IsAdjointPair B₁ B₁' (f₁ - f₁') (g₁ - g₁') := fun x y => by
-  rw [LinearMap.sub_apply, LinearMap.sub_apply, sub_left, sub_right, h, h']
-
-variable {B₂' : BilinForm R M'} {f₂ : M →ₗ[R] M'} {g₂ : M' →ₗ[R] M}
-
-theorem IsAdjointPair.smul (c : R) (h : IsAdjointPair B B₂' f₂ g₂) :
-    IsAdjointPair B B₂' (c • f₂) (c • g₂) := fun x y => by
-  rw [LinearMap.smul_apply, LinearMap.smul_apply, smul_left, smul_right, h]
-
-variable {M'' : Type*} [AddCommMonoid M''] [Module R M'']
-variable (B'' : BilinForm R M'')
-
-theorem IsAdjointPair.comp {f' : M' →ₗ[R] M''} {g' : M'' →ₗ[R] M'} (h : IsAdjointPair B B' f g)
-    (h' : IsAdjointPair B' B'' f' g') : IsAdjointPair B B'' (f'.comp f) (g.comp g') := fun x y => by
-  rw [LinearMap.comp_apply, LinearMap.comp_apply, h', h]
-
-theorem IsAdjointPair.mul {f g f' g' : Module.End R M} (h : IsAdjointPair B B f g)
-    (h' : IsAdjointPair B B f' g') : IsAdjointPair B B (f * f') (g' * g) := fun x y => by
-  rw [LinearMap.mul_apply, LinearMap.mul_apply, h, h']
-
-variable (B B' B₁ B₂) (F₂ : BilinForm R M)
-
-/-- The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms
-on the underlying module. In the case that these two forms are identical, this is the usual concept
-of self adjointness. In the case that one of the forms is the negation of the other, this is the
-usual concept of skew adjointness. -/
-def IsPairSelfAdjoint (f : Module.End R M) :=
-  IsAdjointPair B F f f
-
-/-- The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms. -/
-def isPairSelfAdjointSubmodule : Submodule R (Module.End R M) where
-  carrier := { f | IsPairSelfAdjoint B₂ F₂ f }
-  zero_mem' := isAdjointPair_zero
-  add_mem' hf hg := hf.add hg
-  smul_mem' c _ h := h.smul c
-
-@[simp]
-theorem mem_isPairSelfAdjointSubmodule (f : Module.End R M) :
-    f ∈ isPairSelfAdjointSubmodule B₂ F₂ ↔ IsPairSelfAdjoint B₂ F₂ f := Iff.rfl
-
-theorem isPairSelfAdjoint_equiv (e : M' ≃ₗ[R] M) (f : Module.End R M) :
-    IsPairSelfAdjoint B₂ F₂ f ↔
-      IsPairSelfAdjoint (B₂.comp ↑e ↑e) (F₂.comp ↑e ↑e) (e.symm.conj f) := by
-  have hₗ : (F₂.comp ↑e ↑e).compLeft (e.symm.conj f) = (F₂.compLeft f).comp ↑e ↑e := by
-    ext
-    simp [LinearEquiv.symm_conj_apply]
-  have hᵣ : (B₂.comp ↑e ↑e).compRight (e.symm.conj f) = (B₂.compRight f).comp ↑e ↑e := by
-    ext
-    simp [LinearEquiv.conj_apply]
-  have he : Function.Surjective (⇑(↑e : M' →ₗ[R] M) : M' → M) := e.surjective
-  show BilinForm.IsAdjointPair _ _ _ _ ↔ BilinForm.IsAdjointPair _ _ _ _
-  rw [isAdjointPair_iff_compLeft_eq_compRight, isAdjointPair_iff_compLeft_eq_compRight, hᵣ,
-    hₗ, comp_inj _ _ he he]
-
-/-- An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an
-adjoint for itself. -/
-def IsSelfAdjoint (f : Module.End R M) :=
-  IsAdjointPair B B f f
-
-/-- An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation
-serves as an adjoint. -/
-def IsSkewAdjoint (f : Module.End R₁ M₁) :=
-  IsAdjointPair B₁ B₁ f (-f)
-
-theorem isSkewAdjoint_iff_neg_self_adjoint (f : Module.End R₁ M₁) :
-    B₁.IsSkewAdjoint f ↔ IsAdjointPair (-B₁) B₁ f f :=
-  show (∀ x y, B₁ (f x) y = B₁ x ((-f) y)) ↔ ∀ x y, B₁ (f x) y = (-B₁) x (f y) by
-    simp only [LinearMap.neg_apply, BilinForm.neg_apply, BilinForm.neg_right]
-
-/-- The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact
-it is a Jordan subalgebra.) -/
-def selfAdjointSubmodule :=
-  isPairSelfAdjointSubmodule B B
-
-@[simp]
-theorem mem_selfAdjointSubmodule (f : Module.End R M) :
-    f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint f :=
-  Iff.rfl
-
-/-- The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact
-it is a Lie subalgebra.) -/
-def skewAdjointSubmodule :=
-  isPairSelfAdjointSubmodule (-B₁) B₁
-
-@[simp]
-theorem mem_skewAdjointSubmodule (f : Module.End R₁ M₁) :
-    f ∈ B₁.skewAdjointSubmodule ↔ B₁.IsSkewAdjoint f := by
-  rw [isSkewAdjoint_iff_neg_self_adjoint]
-  exact Iff.rfl
-
-end LinearAdjoints
-
 end BilinForm
 
 namespace BilinForm

Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

@@ -297,34 +297,13 @@ variable {n : Type*} [Fintype n]
 variable (b : Basis n R₂ M₂)
 variable (J J₃ A A' : Matrix n n R₂)
 
-@[simp]
-theorem isAdjointPair_toBilin' [DecidableEq n] :
-    BilinForm.IsAdjointPair (Matrix.toBilin' J) (Matrix.toBilin' J₃) (Matrix.toLin' A)
-        (Matrix.toLin' A') ↔
-      Matrix.IsAdjointPair J J₃ A A' :=
-  isAdjointPair_toLinearMap₂' _ _ _ _
-
-@[simp]
-theorem isAdjointPair_toBilin [DecidableEq n] :
-    BilinForm.IsAdjointPair (Matrix.toBilin b J) (Matrix.toBilin b J₃) (Matrix.toLin b b A)
-        (Matrix.toLin b b A') ↔
-      Matrix.IsAdjointPair J J₃ A A' :=
-  isAdjointPair_toLinearMap₂ _ _ _ _ _ _
-
 theorem Matrix.isAdjointPair_equiv' [DecidableEq n] (P : Matrix n n R₂) (h : IsUnit P) :
     (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A A' ↔
       J.IsAdjointPair J (P * A * P⁻¹) (P * A' * P⁻¹) :=
   Matrix.isAdjointPair_equiv _ _ _ _ h
 
 variable [DecidableEq n]
 
-/-- The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
-given matrices `J`, `J₂`. -/
-def pairSelfAdjointMatricesSubmodule' : Submodule R₂ (Matrix n n R₂) :=
-  (BilinForm.isPairSelfAdjointSubmodule (Matrix.toBilin' J) (Matrix.toBilin' J₃)).map
-    ((LinearMap.toMatrix' : ((n → R₂) →ₗ[R₂] n → R₂) ≃ₗ[R₂] Matrix n n R₂) :
-      ((n → R₂) →ₗ[R₂] n → R₂) →ₗ[R₂] Matrix n n R₂)
-
 theorem mem_pairSelfAdjointMatricesSubmodule' :
     A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ Matrix.IsAdjointPair J J₃ A A := by
   simp only [mem_pairSelfAdjointMatricesSubmodule]

Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

@@ -90,13 +90,13 @@ lemma reflective_reflection (hSB : LinearMap.IsSymm B) {y : M}
     (hx : IsReflective B x) (hy : IsReflective B y) :
     IsReflective B (Module.reflection (coroot_apply_self B hx) y) := by
   constructor
-  · rw [← LinearEquiv.coe_coe, isOrthogonal_reflection B hx hSB]
+  · rw [isOrthogonal_reflection B hx hSB]
     exact hy.1
   · intro z
     have hz : Module.reflection (coroot_apply_self B hx)
         (Module.reflection (coroot_apply_self B hx) z) = z := by
       exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl
-    rw [← hz, ← LinearEquiv.coe_coe, isOrthogonal_reflection B hx hSB,
+    rw [← hz, isOrthogonal_reflection B hx hSB,
       isOrthogonal_reflection B hx hSB]
     exact hy.2 _
 
@@ -170,7 +170,7 @@ def ofBilinear [IsReflexive R M] (B : M →ₗ[R] M →ₗ[R] R) (hNB : LinearMa
     simp only [mem_setOf_eq, PerfectPairing.flip_apply_apply, mul_sub,
       apply_self_mul_coroot_apply B y.2, ← mul_assoc]
     rw [← isOrthogonal_reflection B x.2 hSB y y, apply_self_mul_coroot_apply, ← hSB z, ← hSB z,
-      RingHom.id_apply, RingHom.id_apply, LinearEquiv.coe_coe, Module.reflection_apply, map_sub,
+      RingHom.id_apply, RingHom.id_apply, Module.reflection_apply, map_sub,
       mul_sub, sub_eq_sub_iff_comm, sub_left_inj]
     refine x.2.1.1 ?_
     simp only [mem_setOf_eq, map_smul, smul_eq_mul]

Mathlib/LinearAlgebra/SesquilinearForm.lean

@@ -15,8 +15,8 @@ form `M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M`, where `I₁ : R₁ →+* R`
 Sesquilinear forms are the special case that `M₁ = M₂`, `M = R₁ = R₂ = R`, and `I₁ = RingHom.id R`.
 Taking additionally `I₂ = RingHom.id R`, then one obtains bilinear forms.
 
-These forms are a special case of the bilinear maps defined in `BilinearMap.lean` and all basic
-lemmas about construction and elementary calculations are found there.
+Sesquilinear maps are a special case of the bilinear maps defined in `BilinearMap.lean` and `many`
+basic lemmas about construction and elementary calculations are found there.
 
 ## Main declarations
 
@@ -410,7 +410,7 @@ variable (B B' f g)
 
 /-- Given a pair of modules equipped with bilinear maps, this is the condition for a pair of
 maps between them to be mutually adjoint. -/
-def IsAdjointPair :=
+def IsAdjointPair (f : M → M₁) (g : M₁ → M) :=
   ∀ x y, B' (f x) y = B x (g y)
 
 variable {B B' f g}
@@ -423,17 +423,24 @@ theorem isAdjointPair_iff_comp_eq_compl₂ : IsAdjointPair B B' f g ↔ B'.comp
   · intro _ _
     rw [← compl₂_apply, ← comp_apply, h]
 
-theorem isAdjointPair_zero : IsAdjointPair B B' 0 0 := fun _ _ ↦ by simp only [zero_apply, map_zero]
+theorem isAdjointPair_zero : IsAdjointPair B B' 0 0 := fun _ _ ↦ by
+  simp only [Pi.zero_apply, map_zero, zero_apply]
 
-theorem isAdjointPair_id : IsAdjointPair B B 1 1 := fun _ _ ↦ rfl
+theorem isAdjointPair_id : IsAdjointPair B B (_root_.id : M → M) (_root_.id : M → M) :=
+  fun _ _ ↦ rfl
 
-theorem IsAdjointPair.add (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') :
+theorem isAdjointPair_one : IsAdjointPair B B (1 : Module.End R M) (1 : Module.End R M) :=
+  isAdjointPair_id
+
+theorem IsAdjointPair.add {f f' : M → M₁} {g g' : M₁ → M} (h : IsAdjointPair B B' f g)
+    (h' : IsAdjointPair B B' f' g') :
     IsAdjointPair B B' (f + f') (g + g') := fun x _ ↦ by
-  rw [f.add_apply, g.add_apply, B'.map_add₂, (B x).map_add, h, h']
+  rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, h, h']
 
-theorem IsAdjointPair.comp {f' : M₁ →ₗ[R] M₂} {g' : M₂ →ₗ[R] M₁} (h : IsAdjointPair B B' f g)
-    (h' : IsAdjointPair B' B'' f' g') : IsAdjointPair B B'' (f'.comp f) (g.comp g') := fun _ _ ↦ by
-  rw [LinearMap.comp_apply, LinearMap.comp_apply, h', h]
+theorem IsAdjointPair.comp {f : M → M₁} {g : M₁ → M} {f' : M₁ → M₂} {g' : M₂ → M₁}
+    (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B' B'' f' g') :
+    IsAdjointPair B B'' (f' ∘ f) (g ∘ g') := fun _ _ ↦ by
+  rw [Function.comp_def, Function.comp_def, h', h]
 
 theorem IsAdjointPair.mul {f g f' g' : Module.End R M} (h : IsAdjointPair B B f g)
     (h' : IsAdjointPair B B f' g') : IsAdjointPair B B (f * f') (g' * g) :=
@@ -448,11 +455,11 @@ variable [AddCommGroup M] [Module R M]
 variable [AddCommGroup M₁] [Module R M₁]
 variable [AddCommGroup M₂] [Module R M₂]
 variable {B F : M →ₗ[R] M →ₗ[R] M₂} {B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂}
-variable {f f' : M →ₗ[R] M₁} {g g' : M₁ →ₗ[R] M}
+variable {f f' : M → M₁} {g g' : M₁ → M}
 
 theorem IsAdjointPair.sub (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') :
     IsAdjointPair B B' (f - f') (g - g') := fun x _ ↦ by
-  rw [f.sub_apply, g.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
+  rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']
 
 theorem IsAdjointPair.smul (c : R) (h : IsAdjointPair B B' f g) :
     IsAdjointPair B B' (c • f) (c • g) := fun _ _ ↦ by
@@ -463,7 +470,7 @@ end AddCommGroup
 section OrthogonalMap
 
 variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
-  (B : LinearMap.BilinForm R M) (f : Module.End R M)
+  (B : LinearMap.BilinForm R M) (f : M → M)
 
 /-- A linear transformation `f` is orthogonal with respect to a bilinear form `B` if `B` is
 bi-invariant with respect to `f`. -/
@@ -473,17 +480,17 @@ def IsOrthogonal : Prop :=
 variable {B f}
 
 @[simp]
-lemma _root_.LinearEquiv.isAdjointPair_symm_iff {f : M ≃ₗ[R] M} :
+lemma _root_.LinearEquiv.isAdjointPair_symm_iff {f : M ≃ M} :
     LinearMap.IsAdjointPair B B f f.symm ↔ B.IsOrthogonal f :=
   ⟨fun hf x y ↦ by simpa using hf x (f y), fun hf x y ↦ by simpa using hf x (f.symm y)⟩
 
-lemma isOrthogonal_of_forall_apply_same
-    (h : IsLeftRegular (2 : R)) (hB : B.IsSymm) (hf : ∀ x, B (f x) (f x) = B x x) :
+lemma isOrthogonal_of_forall_apply_same {F : Type*} [FunLike F M M] [LinearMapClass F R M M]
+    (f : F) (h : IsLeftRegular (2 : R)) (hB : B.IsSymm) (hf : ∀ x, B (f x) (f x) = B x x) :
     B.IsOrthogonal f := by
   intro x y
   suffices 2 * B (f x) (f y) = 2 * B x y from h this
   have := hf (x + y)
-  simp only [map_add, add_apply, hf x, hf y, show B y x = B x y from hB.eq y x] at this
+  simp only [map_add, LinearMap.add_apply, hf x, hf y, show B y x = B x y from hB.eq y x] at this
   rw [show B (f y) (f x) = B (f x) (f y) from hB.eq (f y) (f x)] at this
   simp only [add_assoc, add_right_inj] at this
   simp only [← add_assoc, add_left_inj] at this
@@ -510,12 +517,12 @@ variable (B F : M →ₗ[R] M →ₛₗ[I] M₁)
 on the underlying module. In the case that these two maps are identical, this is the usual concept
 of self adjointness. In the case that one of the maps is the negation of the other, this is the
 usual concept of skew adjointness. -/
-def IsPairSelfAdjoint (f : Module.End R M) :=
+def IsPairSelfAdjoint (f : M → M) :=
   IsAdjointPair B F f f
 
 /-- An endomorphism of a module is self-adjoint with respect to a bilinear map if it serves as an
 adjoint for itself. -/
-protected def IsSelfAdjoint (f : Module.End R M) :=
+protected def IsSelfAdjoint (f : M → M) :=
   IsAdjointPair B B f f
 
 end AddCommMonoid
@@ -535,7 +542,7 @@ def isPairSelfAdjointSubmodule : Submodule R (Module.End R M) where
 
 /-- An endomorphism of a module is skew-adjoint with respect to a bilinear map if its negation
 serves as an adjoint. -/
-def IsSkewAdjoint (f : Module.End R M) :=
+def IsSkewAdjoint (f : M → M) :=
   IsAdjointPair B B f (-f)
 
 /-- The set of self-adjoint endomorphisms of a module with bilinear map is a submodule. (In fact
@@ -557,7 +564,7 @@ theorem mem_isPairSelfAdjointSubmodule (f : Module.End R M) :
 
 theorem isPairSelfAdjoint_equiv (e : M₁ ≃ₗ[R] M) (f : Module.End R M) :
     IsPairSelfAdjoint B F f ↔
-      IsPairSelfAdjoint (B.compl₁₂ ↑e ↑e) (F.compl₁₂ ↑e ↑e) (e.symm.conj f) := by
+      IsPairSelfAdjoint (B.compl₁₂ e e) (F.compl₁₂ e e) (e.symm.conj f) := by
   have hₗ :
     (F.compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M)).comp (e.symm.conj f) =
       (F.comp f).compl₁₂ (↑e : M₁ →ₗ[R] M) (↑e : M₁ →ₗ[R] M) := by
@@ -573,7 +580,7 @@ theorem isPairSelfAdjoint_equiv (e : M₁ ≃ₗ[R] M) (f : Module.End R M) :
   have he : Function.Surjective (⇑(↑e : M₁ →ₗ[R] M) : M₁ → M) := e.surjective
   simp_rw [IsPairSelfAdjoint, isAdjointPair_iff_comp_eq_compl₂, hₗ, hᵣ, compl₁₂_inj he he]
 
-theorem isSkewAdjoint_iff_neg_self_adjoint (f : Module.End R M) :
+theorem isSkewAdjoint_iff_neg_self_adjoint (f : M → M) :
     B.IsSkewAdjoint f ↔ IsAdjointPair (-B) B f f :=
   show (∀ x y, B (f x) y = B x ((-f) y)) ↔ ∀ x y, B (f x) y = (-B) x (f y) by simp