eq_zero_or_one_of_pow_of_not_isUnit

English

In a monoid, if x^n is squarefree and x is not a unit, then n=0 or n=1.

Русский

В моноиде, если x^n квадратно свободно и x не является единицей, то n = 0 или n = 1.

LaTeX

$$$\mathrm{Squarefree}(x^{n}) \land \lnot \mathrm{IsUnit}(x) \rightarrow (n=0) \/ (n=1)$$$

Lean4

theorem eq_zero_or_one_of_pow_of_not_isUnit [Monoid R] {x : R} {n : ℕ} (h : Squarefree (x ^ n)) (h' : ¬IsUnit x) :
    n = 0 ∨ n = 1 := by
  contrapose! h'
  replace h' : 2 ≤ n := by omega
  have : x * x ∣ x ^ n := by rw [← sq]; exact pow_dvd_pow x h'
  exact h.squarefree_of_dvd this x (refl _)

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