isRadical_iff_squarefree_of_ne_zero

Mathlib.Algebra.Squarefree.Basic

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

English

For h ≠ 0, IsRadical x is equivalent to Squarefree x.

Русский

При h ≠ 0 IsRadical x эквивалентно Squarefree x.

LaTeX

$$$\mathrm{IsRadical}(x) \iff \mathrm{Squarefree}(x)$ (при $x \neq 0$)$$

Lean4

theorem isRadical_iff_squarefree_of_ne_zero (h : x ≠ 0) : IsRadical x ↔ Squarefree x :=
  ⟨IsRadical.squarefree h, Squarefree.isRadical⟩

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

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

Разделы

Аффилиация

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