ids

Mathlib.Algebra.Ring.CompTypeclasses

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

English

The identity ring homomorphism id_R is surjective.

Русский

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

LaTeX

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

Lean4

instance ids : RingHomSurjective (RingHom.id R₁) :=
  ⟨is_surjective⟩

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

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

Разделы

Аффилиация

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