of_mul_right

Mathlib.Algebra.Squarefree.Basic

URI: https://scilib.ai/kg/mathlib#Squarefree.of_mul_right

English

If the product m⋅n is squarefree, then n is squarefree.

Русский

Если произведение m⋅n квадратно свободно, то n квадратно свободно.

LaTeX

$$$\mathrm{Squarefree}(m n) \rightarrow \mathrm{Squarefree}(n)$$$

Lean4

theorem of_mul_right [CommMonoid R] {m n : R} (hmn : Squarefree (m * n)) : Squarefree n := fun p hp =>
  hmn p (dvd_mul_of_dvd_right hp m)

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

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

Разделы

Аффилиация

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