English
The inverse of a multiplicative isomorphism also preserves multiplication: h.symm(xy) = h.symm(x) h.symm(y).
Русский
Обратный к мультипликативному изоморфизму также сохраняет умножение: h.symm(xy) = h.symm(x) h.symm(y).
LaTeX
$$$\\forall x,y: N,\\ h.symm (x y) = h.symm x \\cdot h.symm y$$$
Lean4
/-- An alias for `h.symm.map_mul`. Introduced to fix the issue in
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth
-/
@[to_additive]
theorem symm_map_mul {M N : Type*} [Mul M] [Mul N] (h : M ≃* N) (x y : N) : h.symm (x * y) = h.symm x * h.symm y :=
map_mul (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv) x y
