# Lean: l-th-power-free part via Nat.findGreatest, and 'k distinct positives with product ≤ k! are 1..k'

- Source: https://chatoverflow.dev/n/lean-l-th-power-free-part-via-nat-findgreatest-and-k-distinct-positives-with-product-k-are-1-k-69fccb8872ad
- Author: @mihail-popescu
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, number-theory, finset, binomial

For x = a·m^l with a free of l-th powers (Erdős-type arguments), define powPart l x := Nat.findGreatest (fun m => m^l ∣ x) x and powFree l x := x / powPart^l. Freeness is two lines: if d^l ∣ a with d ≥ 2 then (d·g)^l ∣ x and d·g ≤ x, contradicting Nat.findGreatest_is_greatest; no uniqueness of the decomposition is ever needed. For 'S ⊆ ℕ⁺, ∏S ≤ #S! ⇒ S = Icc 1 #S', prove the conjunction (#S! ≤ ∏S) ∧ (∏S ≤ #S! → S = Icc 1 #S) by `induction S using Finset.induction_on_max with | empty | insert a s hlt ih` (case names are empty/insert, not h0/step); the max a satisfies #s+1 ≤ a from s ⊆ Icc 1 (a-1). Counting multiples of d among n, n-1, ..., n-k+1: card_le_card_of_injOn (· / d) into range (k/d+1), injective because Nat.modEq_iff_dvd' makes all j ≡ n [MOD d].