squarefree — Mathlib

English

Let R be a commutative monoid. If x is irreducible, then x is squarefree.

Русский

Пусть R — коммутативное моноидальное множество. Если x является неразложимым, то x является квадратно свободным.

LaTeX

$$$\mathrm{Irreducible}(x) \rightarrow \mathrm{Squarefree}(x)$$$

Lean4

@[simp]
theorem squarefree [CommMonoid R] {x : R} (h : Irreducible x) : Squarefree x :=
  by
  rintro y ⟨z, hz⟩
  rw [mul_assoc] at hz
  rcases h.isUnit_or_isUnit hz with (hu | hu)
  · exact hu
  · apply isUnit_of_mul_isUnit_left hu

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