canonicalEquiv_self — Mathlib

English

The canonical equivalence from a localization to itself is the identity map.

Русский

Каноническое отображение от локализации к самой себе — тождественное отображение.

LaTeX

$$$\mathrm{canonicalEquiv}\; S\; P\; P = \mathrm{RingEquiv.refl}\\_ {\ FractionalIdeal\; S\; P}$$$

Lean4

@[simp]
theorem canonicalEquiv_self : canonicalEquiv S P P = RingEquiv.refl _ :=
  by
  rw [← canonicalEquiv_trans_canonicalEquiv S P P]
  convert (canonicalEquiv S P P).symm_trans_self
  exact (canonicalEquiv_symm S P P).symm

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