inverse_id

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.inverse_id

English

Inverse apply on the right side: (g ∘ f).inverse v = f.inverse (g.inverse v).

Русский

Применение обратной справа: $(g \circ f)^{-1} v = f^{-1}(g^{-1} v)$.

LaTeX

$$$(g \circ_L f).inverse v = f.inverse (g.inverse v)$$$

Lean4

@[simp]
theorem inverse_id : (ContinuousLinearMap.id R M).inverse = .id R M :=
  by
  rw [← ringInverse_eq_inverse]
  exact Ring.inverse_one _

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

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

Разделы

Аффилиация

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