coe_mk — Mathlib

English

From a bijection f: M ≃ N that preserves multiplication, the multiplicative isomorphism constructed from f is precisely f as a function.

Русский

Из биекции f: M ≃ N, сохраняющей умножение, мультипликативный изоморфизм, получаемый из f, совпадает с самой функцией f.

LaTeX

$$$(\\mathrm{mk} f hf : M \\to N) = f$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mk (f : M ≃ N) (hf : ∀ x y, f (x * y) = f x * f y) : (mk f hf : M → N) = f :=
  rfl

Похожие утверждения