instFaithfulSMulNatOfCharZero

Mathlib.Algebra.Algebra.Basic

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

English

If [CharZero R], then there is a FaithfulSMul Nat on R.

Русский

Если [CharZero R], существует верное действие ℕ на R.

LaTeX

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

Lean4

instance [CharZero R] : FaithfulSMul ℕ R := by
  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℕ R).injective_nat

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

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

Разделы

Аффилиация

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