squarefree_iff_emultiplicity_le_one

English

In a commutative monoid, Squarefree r is equivalent to: for all x, emultiplicity x r ≤ 1 or IsUnit x.

Русский

В коммутативном моноиде квадратность r эквивалентна: для всех x эмпотомуплотность x в r ≤ 1 или x является единицей.

LaTeX

$$$\mathrm{Squarefree}(r) \iff \forall x, \mathrm{emultiplicity}(x,r) \le 1 \lor \mathrm{IsUnit}(x)$$$

Lean4

theorem squarefree_iff_emultiplicity_le_one [CommMonoid R] (r : R) :
    Squarefree r ↔ ∀ x : R, emultiplicity x r ≤ 1 ∨ IsUnit x :=
  by
  refine forall_congr' fun a => ?_
  rw [← sq, pow_dvd_iff_le_emultiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]
  norm_cast
  rw [← one_add_one_eq_two]
  exact Order.add_one_le_iff_of_not_isMax (by simp)

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