instCharZero

Mathlib.Algebra.Ring.Subsemiring.Basic

URI: https://scilib.ai/kg/mathlib#SubsemiringClass.instCharZero

English

If R has CharZero, then any Subsemiring s of R also has CharZero.

Русский

Если у кольца R характеристика ноль, то любая подсистема (подкольцо) s кольца R тоже имеет CharZero.

LaTeX

$$[CharZero R] → CharZero s$$

Lean4

instance instCharZero [CharZero R] : CharZero s :=
  ⟨Function.Injective.of_comp (f := Subtype.val) (g := Nat.cast (R := s)) Nat.cast_injective⟩

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

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

Разделы

Аффилиация

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