canonicalEquiv_trans_canonicalEquiv

English

The canonical equivalences compose associatively: (canonicalEquiv S P P').trans (canonicalEquiv S P' P'') = canonicalEquiv S P P''.

Русский

Канонические эквивалентности компонуются ассоциативно: (canonicalEquiv S P P').trans (canonicalEquiv S P' P'') = canonicalEquiv S P P''.

LaTeX

$$$(canonicalEquiv\,S\,P\,P').trans (canonicalEquiv\,S\,P'\,P'') = canonicalEquiv\,S\,P\,P''$$$

Lean4

theorem canonicalEquiv_trans_canonicalEquiv (P'' : Type*) [CommRing P''] [Algebra R P''] [IsLocalization S P''] :
    (canonicalEquiv S P P').trans (canonicalEquiv S P' P'') = canonicalEquiv S P P'' :=
  RingEquiv.ext (canonicalEquiv_canonicalEquiv S P P' P'')

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