isInteger_mul

Mathlib.RingTheory.Localization.Integer

URI: https://scilib.ai/kg/mathlib#IsLocalization.isInteger_mul

English

If a and b are integers, then a b is an integer.

Русский

Если a и b целые, то произведение целое.

LaTeX

$$IsLocalization.isInteger_mul$$

Lean4

theorem isInteger_mul {a b : S} (ha : IsInteger R a) (hb : IsInteger R b) : IsInteger R (a * b) :=
  Subsemiring.mul_mem _ ha hb

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

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

Разделы

Аффилиация

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