English
The same compatibility holds for opposite-scalar action: (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f when f respects multiplication.
Русский
Аналогично для противоположного действия: (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f при условии сохранения умножения.
LaTeX
$$$ (MulOpposite.op\\ r \\cdot A).map\\ f = MulOpposite.op (f r) \\cdot (A.map\\ f) $$$
Lean4
/-- The scalar action via `mul.toOppositeSMul` is transformed by the same map as the
elements of the matrix, when `f` preserves multiplication. -/
theorem map_op_smul' [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ a₁ a₂, f (a₁ * a₂) = f a₁ * f a₂) :
(MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f :=
ext fun _ _ => hf _ _
