canonicalEquiv_canonicalEquiv — Mathlib

English

The composition of canonical equivalences is associative: applying canonicalEquiv S P P'' to I via P' equals applying canonicalEquiv S P P' to I and then to P''.

Русский

Составление канонических эквивалентностей является ассоциативным: применение canonicalEquiv S P P'' к I через P' эквивалентно применению через P и затем через P''.

LaTeX

$$$ canonicalEquiv S P P'' (canonicalEquiv S P P' I) = canonicalEquiv S P P'' I $$$

Lean4

@[simp]
theorem canonicalEquiv_canonicalEquiv (P'' : Type*) [CommRing P''] [Algebra R P''] [IsLocalization S P'']
    (I : FractionalIdeal S P) : canonicalEquiv S P' P'' (canonicalEquiv S P P' I) = canonicalEquiv S P P'' I :=
  by
  ext
  simp [IsLocalization.map_map]

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