injective_nat

Mathlib.Algebra.Ring.CharZero

URI: https://scilib.ai/kg/mathlib#RingHom.injective_nat

English

In a ring R of characteristic zero, every ring homomorphism f: ℕ →+* R is injective.

Русский

В кольце R с характеристикой нуля любой гомоморфизм ℕ →+* R инъективен.

LaTeX

$$$\\text{CharZero}(R) \\Rightarrow \\operatorname{Injective}(f)$$$

Lean4

theorem injective_nat (f : ℕ →+* R) [CharZero R] : Injective f :=
  Subsingleton.elim (Nat.castRingHom _) f ▸ Nat.cast_injective

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

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

Разделы

Аффилиация

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