English
If A and B are matrices with AB = I and all entries of A lie in a subfield K of a larger field L, then every entry of B also lies in K.
Русский
Если A и B — матрицы такие, что AB = I и все элементы A лежат в подполе K вложенного поля L, то все элементы B лежат в K.
LaTeX
$$If AB = I and A ∈ M_{m×n}(K), B ∈ M_{n×m}(L), then B ∈ M_{n×m}(K).$$
Lean4
theorem mem_subfield_of_mul_eq_one_of_mem_subfield_right (h_mem : ∀ i j, A i j ∈ K) (i : n) (j : m) : B i j ∈ K :=
by
cases nonempty_fintype m
let A' : Matrix m m K := of fun i j ↦ ⟨A.submatrix id e i j, h_mem i (e j)⟩
have hA' : A'.map K.subtype = A.submatrix id e := rfl
have hA : IsUnit A' :=
by
have h_unit : IsUnit (A.submatrix id e) := isUnit_of_right_inverse (B := B.submatrix e id) (by simpa)
have h_det : (A.submatrix id e).det = K.subtype A'.det := by simp [A', K.subtype.map_det, map, submatrix]
simpa [isUnit_iff_isUnit_det, h_det] using h_unit
obtain ⟨B', hB⟩ := exists_right_inverse_iff_isUnit.mpr hA
suffices (B'.submatrix e.symm id).map K.subtype = B by simp [← this]
replace hB : A * (B'.submatrix e.symm id).map K.subtype = 1 :=
by
replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
simp_rw [Matrix.map_mul] at hB
rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB
simpa using hB
classical simpa [← Matrix.mul_assoc, (mul_eq_one_comm_of_equiv e).mp hAB] using congr_arg (B * ·) hB
