English
If k is a prime divisor of n and k^2 does not divide n, and MinSqFacProp(n/k) holds, then MinSqFacProp(n) holds with a lifted structure.
Русский
Если k простое делит n и k^2 не делит n, и MinSqFacProp(n/k) выполняется, то MinSqFacProp(n) выполняется.
LaTeX
$$$\\forall n\\,\\forall k\\,(Prime(k) \\land k|n \\land \\neg (k^2|n) \\land MinSqFacProp(n/k, o)) \\rightarrow MinSqFacProp(n, o)$$$
Lean4
theorem minSqFacProp_div (n) {k} (pk : Prime k) (dk : k ∣ n) (dkk : ¬k * k ∣ n) {o} (H : MinSqFacProp (n / k) o) :
MinSqFacProp n o :=
by
have : ∀ p, Prime p → p * p ∣ n → k * (p * p) ∣ n := fun p pp dp =>
have :=
(coprime_primes pk pp).2 fun e => by
subst e
contradiction
(coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp
rcases o with - | d
· rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H ⊢
exact fun p pp dp => H p pp ((dvd_div_iff_mul_dvd dk).2 (this _ pp dp))
· obtain ⟨H1, H2, H3⟩ := H
simp only [dvd_div_iff_mul_dvd dk] at H2 H3
exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩
