squarefree_radical

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#UniqueFactorizationMonoid.squarefree_radical

English

The radical of any element is squarefree.

Русский

радикал любого элемента является квадратно-свободным.

LaTeX

$$$ Squarefree( radical(a) ) $$$

Lean4

theorem squarefree_radical : Squarefree (radical a) :=
  by
  nontriviality M
  exact isRadical_radical.squarefree (by simp [radical_ne_zero])

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

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

Разделы

Аффилиация

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