∀ {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃}
  {f g f' g' : Module.End R M},
  B.IsAdjointPair B ⇑f ⇑g → B.IsAdjointPair B ⇑f' ⇑g' → B.IsAdjointPair B ⇑(f * f') ⇑(g' * g)