isInteger_smul

Mathlib.RingTheory.Localization.Integer

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

← MathLib Explorer

English

If b is integer, then a · b is integer for any a.

Русский

Если b целое, тогда для любых a верно, что a·b целое.

LaTeX

$$IsLocalization.isInteger_smul$$

Lean4

theorem isInteger_smul {a : R} {b : S} (hb : IsInteger R b) : IsInteger R (a • b) :=
  by
  rcases hb with ⟨b', hb⟩
  use a * b'
  rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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