canonicalEquiv_flip — Mathlib

English

The canonicalEquiv flip identity states that composing canonicalEquiv with its inverse yields the identity on fractional ideals.

Русский

Сочетание канонической эквивалентности с её обратной дает тождественный отображение на дробных идеалах.

LaTeX

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

Lean4

theorem canonicalEquiv_flip (I) : canonicalEquiv S P P' (canonicalEquiv S P' P I) = I := by
  rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]

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