cast_dvd_cast

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.cast_dvd_cast

English

If m divides n in integers, then their images divide in any ring α: (m : α) ∣ (n : α).

Русский

Если m делит n в целых, то их образы в α делят друг друга.

LaTeX

$$$ \forall {\alpha} [Ring \alpha] (m,n : \mathbb{Z}),\ m \mid n \Rightarrow (m : \alpha) \mid (n : \alpha).$$$

Lean4

theorem cast_dvd_cast [Ring α] (m n : ℤ) (h : m ∣ n) : (m : α) ∣ (n : α) :=
  map_dvd (Int.castRingHom α) h

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

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

Разделы

Аффилиация

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