English
From a homeomorphism f that preserves multiplication, construct a continuous multiplicative isomorphism mk' f h, with the underlying function equal to f.
Русский
Из гомеоморфизма f, сохраняющего умножение, строится непрерывный мультипликативный эквивалент mk' f h, имеющий базовую функцию равной f.
LaTeX
$$$\mathrm{mk'}(f,h)\in M\simeq_{\text{mult}} N \quad\text{and}\quad \mathrm{toFun}(\mathrm{mk'}(f,h))=f.$$$
Lean4
/-- Makes a continuous multiplicative isomorphism from
a homeomorphism which preserves multiplication. -/
@[to_additive /-- Makes an continuous additive isomorphism from
a homeomorphism which preserves addition. -/
]
def mk' (f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃ₜ* N :=
⟨⟨f.toEquiv, h⟩, f.continuous_toFun, f.continuous_invFun⟩
