instFaithfulSMulIntOfCharZero

Mathlib.Algebra.Algebra.Basic

URI: https://scilib.ai/kg/mathlib#instFaithfulSMulIntOfCharZero

← MathLib Explorer

English

If R is a ring with CharZero, then FaithfulSMul ℤ R holds.

Русский

Если R — кольцо с CharZero, то действует верная ℤ-скаляри на R.

LaTeX

$$$[Ring\; R]\;[CharZero\; R] \Rightarrow \mathrm{FaithfulSMul}\; \mathbb{Z}\; R.$$$

Lean4

instance (R : Type*) [Ring R] [CharZero R] : FaithfulSMul ℤ R := by
  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℤ R).injective_int

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

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

Разделы

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

Аффилиация

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