isInteger_add

Mathlib.Algebra.Module.LocalizedModule.Int

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

English

If x and y are integers (with respect to f), then x+y is also an integer.

Русский

Если x и y целые, то x+y тоже целое.

LaTeX

$$$\forall x,y:\, \operatorname{IsInteger}(f,x) \land \operatorname{IsInteger}(f,y) \Rightarrow \operatorname{IsInteger}(f,x+y)$$$

Lean4

theorem isInteger_add {x y : M'} (hx : IsInteger f x) (hy : IsInteger f y) : IsInteger f (x + y) :=
  Submodule.add_mem _ hx hy

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

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

Разделы

Аффилиация

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