Theorems · Definition · linear algebra

Matrix.transposeLinearEquiv

(m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_7) →
      (α : Type u_11) →
        [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → Matrix m n α ≃ₗ[R] Matrix n m α

Matrix.transpose as a LinearMap

Defined in

Mathlib.Data.Matrix.Basic

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModule