Theorems · Theorem · nonassociative algebras

Matrix.reindexLieEquiv_symm

∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {m : Type w₁}
  [inst_3 : DecidableEq m] [inst_4 : Fintype m] (e : n ≃ m),
  (Matrix.reindexLieEquiv e).symm = Matrix.reindexLieEquiv e.symm

Defined in: Mathlib.Algebra.Lie.Matrix
Cited by: 0 results in Mathlib
Foundations: Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing DecidableEq Fintype DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Equivstatement and proof · cited by 8,337
Fintypestatement and proof · cited by 7,736
Matrixstatement · cited by 4,303
Equiv.symmstatement · cited by 3,681
LieRing.ofAssociativeRingstatement · cited by 227
LieEquivstatement · cited by 86
LieEquiv.symmstatement · cited by 34
Matrix.reindexLieEquivstatement · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.