mathlib3 documentation


Invertible matrices over a ring with invariant basis number are square. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem matrix.square_of_invertible {n : Type u_1} {m : Type u_2} [fintype n] [decidable_eq n] [fintype m] [decidable_eq m] {R : Type u_3} [semiring R] [invariant_basis_number R] (M : matrix n m R) (N : matrix m n R) (h : M.mul N = 1) (h' : N.mul M = 1) :