mem_subfield_of_mul_eq_one_of_mem_subfield_left

English

If AB = I and all entries of B lie in a subfield K of a larger field L, then all entries of A lie in K.

Русский

Если AB = I и все элементы B лежат в подполе K, то элементы A также лежат в K.

LaTeX

$$If AB = I and B ∈ M_{n×m}(K), then A ∈ M_{m×n}(K).$$

Lean4

theorem mem_subfield_of_mul_eq_one_of_mem_subfield_left (h_mem : ∀ i j, B i j ∈ K) (i : m) (j : n) : A i j ∈ K :=
  by
  replace hAB : Bᵀ * Aᵀ = 1 := by simpa using congr_arg transpose hAB
  rw [← A.transpose_apply]
  simp_rw [← B.transpose_apply] at h_mem
  exact mem_subfield_of_mul_eq_one_of_mem_subfield_right e K hAB (fun i j ↦ h_mem j i) j i

Похожие утверждения