isInteger_add

Mathlib.RingTheory.Localization.Integer

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

English

If a and b are integers (in the localized sense), then a + b is an integer.

Русский

Если a и b целые, то a + b тоже целое.

LaTeX

$$IsLocalization.isInteger_add$$

Lean4

theorem isInteger_add {a b : S} (ha : IsInteger R a) (hb : IsInteger R b) : IsInteger R (a + b) :=
  Subsemiring.add_mem _ ha hb

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

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

Разделы

Аффилиация

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