Theorems · Theorem · linear algebra

Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left

∀ {m : Type u_1} {n : Type u_2} {L : Type u_3} [Finite m] [inst : Fintype n] [inst_1 : DecidableEq m] [inst_2 : Field L]
  (e : m ≃ n) (K : Subfield L) {A : Matrix m n L} {B : Matrix n m L},
  A * B = 1 → (∀ (i : n) (j : m), B i j ∈ K) → ∀ (i : m) (j : n), A i j ∈ K

Defined in

Mathlib.LinearAlgebra.Matrix.BaseChange

Cited by

1 results in Mathlib

Foundations

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

Assumes

FiniteFintypeDecidableEqField