Theorems · Definition · linear algebra

Matrix.conjTransposeAlgEquiv

(n : Type u_3) →
  {R : Type u_7} →
    (α : Type v) →
      [inst : Fintype n] →
        [inst_1 : CommSemiring R] →
          [inst_2 : StarRing R] →
            [TrivialStar R] →
              [inst_4 : Semiring α] →
                [inst_5 : StarRing α] →
                  [inst_6 : Algebra R α] → [StarModule R α] → Matrix n n α ≃⋆ₐ[R] (Matrix n n α)ᵐᵒᵖ

Matrix.conjTranspose as a StarAlgEquiv to the opposite ring

Defined in

Mathlib.LinearAlgebra.Matrix.ConjTranspose

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeCommSemiringStarRingTrivialStarSemiringStarRingAlgebraStarModule