/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Algebra.Squarefree.Basic@[expose] public sectionvariable {M M₀ : Type*} {r m : M} {k : ℕ}section Monoidvariable [Monoid M]def Powerfree (k : ℕ) (m : M) : Prop := ∀ ⦃x : M⦄, x ^ k ∣ m → IsUnit xtheorem Powerfree.of_le {a b : ℕ} (hab : a ≤ b) (hm : Powerfree a m) : Powerfree b m := fun x hx => hm (dvd_of_mul_right_dvd (pow_mul_pow_sub x hab ▸ hx))theorem Powerfree.of_dvd (hrm : r ∣ m) (hm : Powerfree k m) : Powerfree k r := fun _ hx => hm (hx.trans hrm)theorem powerfree_congr (hrm : Associated r m) : Powerfree k r ↔ Powerfree k m := ⟨fun h => h.of_dvd hrm.dvd', fun h => h.of_dvd hrm.dvd⟩@[simp] theorem powerfree_neg [HasDistribNeg M] : Powerfree k (-m) ↔ Powerfree k m := powerfree_congr (Associated.refl m).neg_left@[simp] theorem powerfree_two {m : M} : Powerfree 2 m ↔ Squarefree m where mp h x hx := h (sq x ▸ hx) mpr h x hx := h x (sq x ▸ hx)end Monoidsection CommMonoidvariable [CommMonoid M]theorem IsUnit.powerfree (h : IsUnit m) (hk : k ≠ 0) : Powerfree k m := fun _ hx => (isUnit_pow_iff hk).1 (isUnit_of_dvd_unit hx h)@[simp] theorem powerfree_one (hk : k ≠ 0) : Powerfree k (1 : M) := isUnit_one.powerfree hk theorem Irreducible.powerfree (h : Irreducible m) (hk : 2 ≤ k) : Powerfree k m := byM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible mhk:2 ≤ k⊢ Powerfree k m rintro y ⟨z, hz⟩M:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible mhk:2 ≤ ky:Mz:Mhz:m = y ^ k * z⊢ IsUnit y induction k with | zero =>zeroM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mhk:2 ≤ 0hz:m = y ^ 0 * z⊢ IsUnit y grindAll goals completed! 🐙 | succ n ih =>succM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ (n + 1) * z⊢ IsUnit y rw [pow_succ,succM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * y * z⊢ IsUnit ysuccM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)⊢ IsUnit y mul_assocsuccM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)⊢ IsUnit ysuccM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)⊢ IsUnit y] at hzsuccM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)⊢ IsUnit y rcases h.isUnit_or_isUnit hz with (hu | hu)succ.inlM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)hu:IsUnit (y ^ n)⊢ IsUnit ysucc.inrM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)hu:IsUnit (y * z)⊢ IsUnit y ·succ.inlM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)hu:IsUnit (y ^ n)⊢ IsUnit y exact (isUnit_pow_iff (byM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)hu:IsUnit (y ^ n)⊢ n ≠ 0 linarithAll goals completed! 🐙)).1 hu ·succ.inrM:Type u_1m:Mk:ℕinst✝:CommMonoid Mh:Irreducible my:Mz:Mn:ℕih:2 ≤ n → m = y ^ n * z → IsUnit yhk:2 ≤ n + 1hz:m = y ^ n * (y * z)hu:IsUnit (y * z)⊢ IsUnit y apply isUnit_of_mul_isUnit_left huAll goals completed! 🐙end CommMonoid @[simp] theorem not_powerfree_zero [MonoidWithZero M₀] [Nontrivial M₀] (k : ℕ) : ¬ Powerfree k (0 : M₀) := byM₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ¬Powerfree k 0 rw [Powerfree,M₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ¬∀ ⦃x : M₀⦄, x ^ k ∣ 0 → IsUnit xM₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ∃ x, ¬(x ^ k ∣ 0 → IsUnit x) not_forallM₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ∃ x, ¬(x ^ k ∣ 0 → IsUnit x)M₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ∃ x, ¬(x ^ k ∣ 0 → IsUnit x)]M₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ∃ x, ¬(x ^ k ∣ 0 → IsUnit x) exact ⟨0, byM₀:Type u_2inst✝¹:MonoidWithZero M₀inst✝:Nontrivial M₀k:ℕ⊢ ¬(0 ^ k ∣ 0 → IsUnit 0) simpAll goals completed! 🐙⟩theorem Prime.powerfree [CommMonoidWithZero M₀] [IsCancelMulZero M₀] {m : M₀} (h : Prime m) (hk : 2 ≤ k) : Powerfree k m := h.irreducible.powerfree hk