Squarefree — Mathlib

English

In a monoid, an element r is squarefree if every x with x^2 dividing r is a unit.

Русский

В моноиде элемент r квадратно свободен, если для любого x, когда x^2 делит r, то x является единицей.

LaTeX

$$$\\text{Squarefree}(r) \\;:=\\; \\forall x:\\ R,\\ x^2 \\mid r \\rightarrow \\text{IsUnit}(x)$$$

Lean4

/-- An element of a monoid is squarefree if the only squares that
  divide it are the squares of units. -/
def Squarefree [Monoid R] (r : R) : Prop :=
  ∀ x : R, x * x ∣ r → IsUnit x

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