Commute.map

theorem Commute.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {x y : M} [inst_2 : FunLike F M N] [inst_3 : MulHomClass F M N], Commute x y → ∀ (f : F), Commute (f x) (f y)

The theorem `Commute.map` states that for any types `F`, `M`, and `N`, given multiplication operations on `M` and `N`, any two elements `x` and `y` of `M` that commute, a function-like from `M` to `N` (`FunLike F M N`), and a multiplication homomorphism from `M` to `N` (`MulHomClass F M N`), the image of the commuting elements under any function `f` of type `F` will also commute. In other words, the property of commuting is preserved under the mapping `f`.

More concisely: Given types `M` and `N`, multiplication operations on `M` and `N`, a function-like `F` from `M` to `N`, a multiplication homomorphism `h` from `M` to `N`, and commuting elements `x` and `y` in `M`, `h(x * y) = h(y * x)`.