Nat.squarefree_iff_nodup_factors
theorem Nat.squarefree_iff_nodup_factors : ∀ {n : ℕ}, n ≠ 0 → (Squarefree n ↔ n.factors.Nodup)
The theorem `Nat.squarefree_iff_nodup_factors` states that for any non-zero natural number `n`, `n` is squarefree if and only if the list of its prime factorization, `Nat.factors n`, has no duplicates. Here, a number is considered squarefree if the only squares that divide it are the squares of units. This theorem provides a characterization of squarefree numbers in terms of the uniqueness of their prime factors.
More concisely: A natural number `n` is squarefree if and only if its prime factorization `Nat.factors n` has no repeating elements.
|
Nat.squarefree_mul
theorem Nat.squarefree_mul : ∀ {m n : ℕ}, m.Coprime n → (Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n)
The theorem `Nat.squarefree_mul` states that the property of being squarefree is multiplicative for natural numbers. Specifically, for any two natural numbers `m` and `n` that are coprime (i.e., their greatest common divisor is 1), the product `m * n` is squarefree if and only if both `m` and `n` are squarefree. Here, a number is considered squarefree if the only squares that divide it are the squares of units. Note that the implication from `Squarefree (m * n)` to `Squarefree m ∧ Squarefree n` does not require the coprimality of `m` and `n` and generalizes to arbitrary commutative monoids.
More concisely: For coprime natural numbers m and n, the product m * n is squarefree if and only if both m and n are squarefree.
|
Nat.minSqFac_has_prop
theorem Nat.minSqFac_has_prop : ∀ (n : ℕ), n.MinSqFacProp n.minSqFac
The theorem `Nat.minSqFac_has_prop` asserts that for every natural number `n`, the function `Nat.minSqFac` satisfies the property `Nat.MinSqFacProp`. In other words, if `Nat.minSqFac` returns `none` for a natural number `n`, then `n` is squarefree, meaning it has no square factor other than 1. If `Nat.minSqFac` returns `some d`, then `d` is a prime number and the smallest square factor of `n`. This means that `d * d` divides `n` and any other prime number `p` whose square divides `n` must be greater than or equal to `d`.
More concisely: For every natural number `n`, if `Nat.minSqFac n` is `none`, then `n` is squarefree, and if `Nat.minSqFac n` is `some d`, then `d` is a prime number and `d^2` is the smallest square factor of `n`.
|