Theorems · Theorem · linear algebra

LinearMap.IsAdjointPair.add

∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {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₁] [inst_5 : AddCommMonoid M₃]
  [inst_6 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {f f' : M → M₁}
  {g g' : M₁ → M}, B.IsAdjointPair B' f g → B.IsAdjointPair B' f' g' → B.IsAdjointPair B' (f + f') (g + g')

Defined in

Mathlib.LinearAlgebra.SesquilinearForm.Basic

Cited by

0 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModule