Theorems · Theorem · linear algebra

Matrix.mul_eq_one_comm_of_equiv

∀ {m : Type u_10} {n : Type u_11} {R : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : MulOne R] [inst_5 : AddCommMonoid R] [IsStablyFiniteRing R] {A : Matrix m n R}
  {B : Matrix n m R} (e : m ≃ n), A * B = 1 ↔ B * A = 1

A version of mul_eq_one_comm that works for square matrices with rectangular types.

Defined in

Mathlib.Data.Matrix.Mul

Cited by

4 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqFintypeDecidableEqMulOneAddCommMonoidIsStablyFiniteRing