Theorems · Theorem · linear algebra

LinearMap.IsSymm.add

∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B C : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → C.IsSymm → (B + C).IsSymm

Defined in

Mathlib.LinearAlgebra.SesquilinearForm.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule