English
The simultaneous left-right multiplication defines a linear map; for each (a,b) ∈ A×A, the map x ↦ a x b is R-linear.
Русский
Одновременное левое-правое умножение задаёт линейное отображение; для каждого (a,b) ∈ A×A отображение x ↦ a x b линейно по отношению к R.
LaTeX
$$$$ mulLeftRight\,R\,(a,b): A \to A, \quad (mulLeftRight\,R\,(a,b))(x) = a x b. $$$$
Lean4
/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are
equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various
specialized `ext` lemmas about `→ₗ[R]` to then be applied.
This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`. -/
theorem map_mul_iff (f : A →ₗ[R] B) :
(∀ x y, f (x * y) = f x * f y) ↔ (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f :=
Iff.symm LinearMap.ext_iff₂
