Theorems · Theorem · linear algebra

LinearMap.isSymm_iff_basis

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {B : M →ₗ⋆[R] M →ₗ[R] R} {ι : Type u_4} (b : Module.Basis ι R M),
  B.IsSymm ↔ ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)

Defined in

Mathlib.LinearAlgebra.SesquilinearForm.Star

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringStarRingAddCommMonoidModule