sumEquivOfFintype_symm_apply

Mathlib.RingTheory.AdicCompletion.Functoriality

URI: https://scilib.ai/kg/mathlib#AdicCompletion.sumEquivOfFintype_symm_apply

English

The inverse of sumEquivOfFintype acts by sumInv: (sumEquivOfFintype I M)⁻¹ x = sumInv I M x.

Русский

Обратное отображение sumEquivOfFintype действует через sumInv: (sumEquivOfFintype I M)⁻¹ x = sumInv I M x.

LaTeX

$$$ (sumEquivOfFintype I M)^{-1} x = sumInv I M x $$$

Lean4

@[simp]
theorem sumEquivOfFintype_symm_apply (x : AdicCompletion I (⨁ j, M j)) :
    (sumEquivOfFintype I M).symm x = sumInv I M x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru