comp_apply_eq₂

Mathlib.Algebra.Ring.CompTypeclasses

URI: https://scilib.ai/kg/mathlib#RingHomInvPair.comp_apply_eq₂

English

If σ and σ' form a RingHomInvPair, then the other composition σ(σ'(x)) equals x for all x ∈ R2.

Русский

Если σ и σ' образуют RingHomInvPair, то композиция σ ∘ σ' равна тождественному отображению на R2.

LaTeX

$$$\sigma(\sigma'(x)) = x$$$

Lean4

theorem comp_apply_eq₂ {x : R₂} : σ (σ' x) = x :=
  by
  rw [← RingHom.comp_apply, comp_eq₂]
  simp

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

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

Разделы

Аффилиация

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