separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂

English

The left-separating property of a bilinear form defined by a matrix is unchanged under a change of basis: for any basis b, (Matrix.toLinearMap₂' R₁ M).SeparatingLeft holds if and only if (Matrix.toLinearMap₂ b b M).SeparatingLeft holds.

Русский

Свойство разделения слева для билинейной формы, заданной матрицей, не зависит от выбора базиса: для любого базиса b справедливо, что (Matrix.toLinearMap₂' R₁ M).SeparatingLeft тогда и только тогда, когда (Matrix.toLinearMap₂ b b M).SeparatingLeft.

LaTeX

$$$(Matrix.toLinearMap₂' R_1\ M).SeparatingLeft\ (R := R_1) \iff (Matrix.toLinearMap₂\ b\ b\ M).SeparatingLeft$$$

Lean4

theorem _root_.Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ {M : Matrix ι ι R₁}
    (b : Basis ι R₁ M₁) :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) ↔ (Matrix.toLinearMap₂ b b M).SeparatingLeft :=
  (separatingLeft_congr_iff b.equivFun.symm b.equivFun.symm).symm

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