isRegular_of_isLeftRegular_det — Mathlib

English

If det(A) is left-regular, then A is regular.

Русский

Если det(A) является леворегулярным элементом кольца, то A является регулярной матрицей.

LaTeX

$$$\text{If } \det(A) \text{ is left-regular, then } A \text{ is regular.}$$$

Lean4

theorem isRegular_of_isLeftRegular_det {A : Matrix n n α} (hA : IsLeftRegular A.det) : IsRegular A :=
  by
  constructor
  · intro B C h
    refine hA.matrix ?_
    simp only at h ⊢
    rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ← adjugate_mul, Matrix.mul_assoc,
      Matrix.mul_assoc, h]
  · intro B C (h : B * A = C * A)
    refine hA.matrix ?_
    simp only
    rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ← mul_adjugate, ←
      Matrix.mul_assoc, ← Matrix.mul_assoc, h]

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