ids

Mathlib.Algebra.Ring.CompTypeclasses

URI: https://scilib.ai/kg/mathlib#RingHomCompTriple.ids

English

Given RingHomInvPair σ σ', the swapped pair RingHomInvPair σ' σ also holds.

Русский

Дано RingHomInvPair σ σ', также выполняется RingHomInvPair σ' σ.

LaTeX

$$RingHomInvPair σ' σ$$

Lean4

instance ids : RingHomCompTriple (RingHom.id R₁) σ₁₂ σ₁₂ :=
  ⟨by simp⟩

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

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

Разделы

Аффилиация

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