coe_toEquiv — Mathlib

English

For any ring isomorphism f: R ≃+* S, the coercion to an equivalence from R to S coincides with the underlying equivalence; i.e., the functorial embedding of a ring isomorphism as a function agrees with its Equiv representation.

Русский

Для любого кольцевого изоморфизма f: R ≃+* S привод к эквивалентности R ≃ S совпадает с его эквивалентностью; то есть приведенный к эквивалентности отображение совпадает с представлением как эквивалентности.

LaTeX

$$$\\big( f : R \\simeq^+_* S \\big) : \\ \\text{⇑}(f : R \\simeq S) = f$$$

Lean4

@[simp]
theorem coe_toEquiv (f : R ≃+* S) : ⇑(f : R ≃ S) = f :=
  rfl

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