toEquiv_eq_coe — Mathlib

English

Let f be a ring isomorphism R ≃+* S. Then the underlying equivalence (the toEquiv component) is exactly the same as viewing f as an equivalence; i.e., f.toEquiv = f when considered as an Equiv between R and S.

Русский

Пусть f — кольцевой изоморфизм R ≃+* S. Тогда соответствующая ему эквивалентность (нижняя составляющая toEquiv) совпадает с эквивалентностью, получаемой при взгляде на f как на эквив between R и S.

LaTeX

$$$f^{\\mathrm{toEquiv}} = f$$$

Lean4

@[simp]
theorem toEquiv_eq_coe (f : R ≃+* S) : f.toEquiv = f :=
  rfl

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