right_ids

Mathlib.Algebra.Ring.CompTypeclasses

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

English

The identity ring homomorphism is surjective as a function.

Русский

Тождественный гомоморфизм является сюръективным функцией.

LaTeX

$$$\text{RingHomSurjective}(\text{RingHom.id }R)$$$

Lean4

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

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

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

Разделы

Аффилиация

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