coe_toEquiv_symm — Mathlib

English

The inverse of a ring isomorphism corresponds to the inverse Equiv; i.e., (e.symm) equals the symm of (e).

Русский

Обратное кольцевого изоморфизма соответствует обратной эквивалентности; то есть e.symm совпадает с симметрией e.

LaTeX

$$$ (e.symm : S \\to R) = (e : R \\to S)^{-1} $$$

Lean4

@[simp]
theorem coe_toEquiv_symm (e : R ≃+* S) : (e.symm : S ≃ R) = (e : R ≃ S).symm :=
  rfl

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