Matrices and base change

This file is a home for results about base change for matrices.

Main results:

• Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right: if an invertible matrix over L takes values in subfield K ⊆ L, then so does its (right) inverse.
• Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left: if an invertible matrix over L takes values in subfield K ⊆ L, then so does its (left) inverse.

theorem Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right {m : Type u_1} {n : Type u_2} {L : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [Field L] (e : m ≃ n) (K : Subfield L) {A : Matrix m n L} {B : Matrix n m L} (hAB : A * B = 1) (h_mem : ∀ (i : m) (j : n), A i j ∈ K) (i : n) (j : m) : B i j ∈ K

theorem Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left {m : Type u_1} {n : Type u_2} {L : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [Field L] (e : m ≃ n) (K : Subfield L) {A : Matrix m n L} {B : Matrix n m L} (hAB : A * B = 1) (h_mem : ∀ (i : n) (j : m), B i j ∈ K) (i : m) (j : n) : A i j ∈ K