squarefree_one

Mathlib.Algebra.Squarefree.Basic

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

English

One is squarefree in any commutative monoid if it is nonzero.

Русский

Единица квадратно свободна в любом коммутативном моноиде при условии ненулевости единицы.

LaTeX

$$[CommMonoid R] Squarefree 1$$

Lean4

theorem squarefree_one [CommMonoid R] : Squarefree (1 : R) :=
  isUnit_one.squarefree

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

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

Разделы

Аффилиация

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