comp_apply_eq

Mathlib.Algebra.Ring.CompTypeclasses

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

English

If σ and σ' form a RingHomInvPair, then σ'(σ(x)) = x for all x ∈ R1.

Русский

Пусть σ и σ' образуют RingHomInvPair; тогда для всех x ∈ R1 выполняется σ'(σ(x)) = x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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