cast_dvd_cast

Mathlib.Data.Nat.Cast.Basic

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

English

Divisibility is preserved by nat cast: if m divides n in ℕ, then (m : α) divides (n : α) in any semiring α.

Русский

Делимость сохраняется при приводе по Nat: если m|n, то (m : α) | (n : α).

LaTeX

$$$ m \mid n \implies (m : \alpha) \mid (n : \alpha) $$$

Lean4

@[gcongr]
theorem cast_dvd_cast (h : m ∣ n) : (m : α) ∣ (n : α) :=
  map_dvd (Nat.castRingHom α) h

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

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

Разделы

Аффилиация

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