Theorems · Theorem · nonassociative algebras

LieAlgebra.Orthogonal.jd_transform

∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  (LieAlgebra.Orthogonal.PD l R).transpose * LieAlgebra.Orthogonal.JD l R * LieAlgebra.Orthogonal.PD l R =
    2 • LieAlgebra.Orthogonal.S l R

Defined in

Mathlib.Algebra.Lie.Classical

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqCommRingFintype