English
For a scalar r and a matrix M of size m×n over α, the left-multiplication by the scalar matrix and the right-multiplication by the scalar matrix are equal exactly when the scalar r acts on M by the standard left action equal to the opposite-right action on entries.
Русский
Для скаляра r и матрицы M размера m×n над α равенство левой и правой скалярной умножения эквивалентно тому, что действие r слева на M совпадает с действием MulOpposite r справа.
LaTeX
$$\operatorname{scalar}_m(r) M = M \operatorname{scalar}_n(r) \iff r \cdot M = \operatorname{MulOpposite.op}(r) \cdot M$$
Lean4
/-- A version of `Matrix.scalar_commute_iff` for rectangular matrices. -/
theorem scalar_comm_iff {r : α} {M : Matrix m n α} : scalar m r * M = M * scalar n r ↔ r • M = MulOpposite.op r • M :=
by simp_rw [scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]
