def Powerfree {M : Type u_1} [Monoid M] (k : ℕ) (m : M) : Prop

Equations

• Powerfree k m = ∀ ⦃x : M⦄, x ^ k ∣ m → IsUnit x

theorem Powerfree.of_le {M : Type u_1} {m : M} [Monoid M] {a b : ℕ} (hab : a ≤ b) (hm : Powerfree a m) : Powerfree b m

theorem Powerfree.of_dvd {M : Type u_1} {r m : M} {k : ℕ} [Monoid M] (hrm : r ∣ m) (hm : Powerfree k m) : Powerfree k r

theorem powerfree_congr {M : Type u_1} {r m : M} {k : ℕ} [Monoid M] (hrm : Associated r m) : Powerfree k r ↔ Powerfree k m

@[simp]

theorem powerfree_neg {M : Type u_1} {m : M} {k : ℕ} [Monoid M] [HasDistribNeg M] : Powerfree k (-m) ↔ Powerfree k m

@[simp]

theorem powerfree_two {M : Type u_1} [Monoid M] {m : M} : Powerfree 2 m ↔ Squarefree m

theorem IsUnit.powerfree {M : Type u_1} {m : M} {k : ℕ} [CommMonoid M] (h : IsUnit m) (hk : k ≠ 0) : Powerfree k m

@[simp]

theorem powerfree_one {M : Type u_1} {k : ℕ} [CommMonoid M] (hk : k ≠ 0) : Powerfree k 1

theorem Irreducible.powerfree {M : Type u_1} {m : M} {k : ℕ} [CommMonoid M] (h : Irreducible m) (hk : 2 ≤ k) : Powerfree k m

@[simp]

theorem not_powerfree_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] (k : ℕ) : ¬Powerfree k 0

theorem Prime.powerfree {M₀ : Type u_2} {k : ℕ} [CommMonoidWithZero M₀] [IsCancelMulZero M₀] {m : M₀} (h : Prime m) (hk : 2 ≤ k) : Powerfree k m