English
There is a multiplicative isomorphism built from a base bijection f: M ≃ N that preserves multiplication, i.e., a structure (M ≃* N) with underlying map f and the corresponding multiplication-preserving property.
Русский
Существует мультипликативный изоморфизм, построенный на базе биекции f: M ≃ N, сохраняющей умножение, то есть структура (M ≃* N) с осн. отображением f и соответствующим свойством сохранения умножения.
LaTeX
$$$\\mathrm{def}\; \\ mk' (f : M \\simeq N) (h : \\forall x,y, f(xy)=f(x)f(y)) : M \\simeq^* N$$$
Lean4
/-- Makes a multiplicative isomorphism from a bijection which preserves multiplication. -/
@[to_additive /-- Makes an additive isomorphism from a bijection which preserves addition. -/
]
def mk' (f : M ≃ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃* N :=
⟨f, h⟩
