English
For a matrix M ∈ Matrix m n α and r ∈ α, the equality scalar m r ⋅ M = M ⋅ scalar n r is equivalent to r acting on M from the left equalling the opposite-right action on M.
Русский
Для матрицы M ∈ Matrix m n α и скаляра r ∈ α равенство scalar m r ⋅ M = M ⋅ scalar n r эквивалентно тому, что левое действие r на M совпадает с правым действием MulOpposite r на M.
LaTeX
$$\operatorname{scalar}_m(r) M = M \operatorname{scalar}_n(r) \iff r \cdot M = MulOpposite.op(r) \cdot M$$
Lean4
/-- A version of `Matrix.scalar_commute` for rectangular matrices. -/
theorem scalar_comm (r : α) (hr : ∀ r', Commute r r') (M : Matrix m n α) : scalar m r * M = M * scalar n r :=
scalar_comm_iff.2 <| ext fun _ _ => hr _
