PosNum.minFac_to_nat

theorem PosNum.minFac_to_nat : ∀ (n : PosNum), ↑n.minFac = (↑n).minFac

This theorem states that for every positive number `n`, the smallest prime factor of `n` when considered as a positive number, is equal to the smallest prime factor of `n` when considered as a natural number. In other words, the function `PosNum.minFac` applied to `n` and then coerced to a natural number, is the same as the function `Nat.minFac` applied to `n` coerced to a natural number. This theorem connects the prime factorization of positive numbers and natural numbers.

More concisely: For every positive integer `n`, the smallest prime factor of `n` as a positive number equals the smallest prime factor of `n` as a natural number. Alternatively, `PosNum.minFac ⁩ n = Nat.minFac ⁩ (n : nat)`.