Theorems · Theorem · linear algebra

LinearMap.IsSymm.eq

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

Defined in

Mathlib.LinearAlgebra.SesquilinearForm.Basic

Cited by

17 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule