LinearMap.map_mul_iff

theorem LinearMap.map_mul_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B), (∀ (x y : A), f (x * y) = f x * f y) ↔ (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f

This theorem states that for any linear map `f` from an `A` algebra over a commutative semiring `R` to a `B` algebra over the same commutative semiring `R`, `f` preserves multiplication if and only if pre- and post-composition with the `LinearMap.mul` are equivalent. In other words, for all elements `x, y` of `A`, the image of the product `x * y` under `f` is equal to the product of the images `f(x)` and `f(y)` if and only if the composite map of `f` with `LinearMap.mul` in `A` is equal to the composite map of `f` with `LinearMap.mul` in `B`. This linear map version of `AddMonoidHom.map_mul_iff` can be particularly useful in simplifying expressions involving linear maps, as it allows for the application of various specialized `ext` lemmas about linear maps.

More concisely: A linear map between two algebras over a commutative semiring preserves multiplication if and only if pre- and post-composition with the linear map multiplication are equivalent.