injective_int

Mathlib.Data.Int.CharZero

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

← MathLib Explorer

English

For any f : ℤ →+* α with CharZero α, f is injective.

Русский

Для любого f: ℤ →+* α с CharZero α функция f инъективна.

LaTeX

$$$\\forall f:\\mathbb{Z}\\to_+*\\alpha\\ ,\\ CharZero(\\alpha)\\Rightarrow Function.Injective f$$$

Lean4

theorem injective_int {α : Type*} [NonAssocRing α] (f : ℤ →+* α) [CharZero α] : Function.Injective f :=
  Subsingleton.elim (Int.castRingHom _) f ▸ Int.cast_injective

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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