instToRingHomRingEquiv

Mathlib.Algebra.Ring.CompTypeclasses

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

English

If σ: R1 ≃+* R2 is a ring equivalence, then the associated RingHom is surjective.

Русский

Если σ: R1 ≃+* R2 — кольцевой эквивалент, то соответствующий RingHom сюръективен.

LaTeX

$$$\forall y \in R_2, \exists x \in R_1: (\text{toRingHom } σ)(x) = y$$$

Lean4

instance (σ : R₁ ≃+* R₂) : RingHomSurjective (σ : R₁ →+* R₂) :=
  ⟨σ.surjective⟩

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

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

Разделы

Аффилиация

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