mapEquiv_refl — Mathlib

English

The mapEquiv of the identity equivalence is the identity ring equivalence on FractionalIdeal S P.

Русский

MapEquiv тождественного эквивалента есть тождественное кольцевое эквивложение на FractionalIdeal S P.

LaTeX

$$$ \\mathrm{mapEquiv}( \\mathrm{AlgEquiv.refl}) = \\mathrm RingEquiv.refl (\\mathrm{FractionalIdeal} S P) $$$

Lean4

@[simp]
theorem mapEquiv_refl : mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P) :=
  RingEquiv.ext fun x => by simp

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