Theorems · Theorem · nonassociative algebras

skewAdjointMatricesLieSubalgebraEquivTranspose_apply

∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n]
  {m : Type w} [inst_3 : DecidableEq m] [inst_4 : Fintype m] (e : Matrix n n R ≃ₐ[R] Matrix m m R)
  (h : ∀ (A : Matrix n n R), (e A).transpose = e A.transpose) (A : ↥(skewAdjointMatricesLieSubalgebra J)),
  ↑((skewAdjointMatricesLieSubalgebraEquivTranspose J e h) A) = e ↑A

Defined in

Mathlib.Algebra.Lie.SkewAdjoint

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFintypeDecidableEqDecidableEqFintype