dvd_nsmul_of_dvd

Mathlib.Algebra.Ring.Divisibility.Lemmas

URI: https://scilib.ai/kg/mathlib#dvd_nsmul_of_dvd

English

In a nonunital semiring R, if x ∣ y, then n • y is divisible by x for every natural number n.

Русский

В неединичном полукольце R, если x делит y, то для каждого натурального числа n, n • y делится на x.

LaTeX

$$$x \mid y \Rightarrow x \mid n \cdot y$$$

Lean4

theorem dvd_nsmul_of_dvd [NonUnitalSemiring R] {x y : R} (n : ℕ) (h : x ∣ y) : x ∣ n • y :=
  dvd_smul_of_dvd n h

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

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

Разделы

Аффилиация

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