minFac_eq_two_iff — Mathlib

English

minFac n = 2 if and only if 2 divides n.

Русский

minFac n = 2 тогда, когда 2 делит n.

LaTeX

$$$\\\\minFac n = 2 \\\\iff 2 \\\\mid n$$$

Lean4

@[simp]
theorem minFac_eq_two_iff (n : ℕ) : minFac n = 2 ↔ 2 ∣ n :=
  by
  constructor
  · intro h
    rw [← h]
    exact minFac_dvd n
  · intro h
    have ub := minFac_le_of_dvd (le_refl 2) h
    have lb := minFac_pos n
    refine ub.eq_or_lt.resolve_right fun h' => ?_
    suffices n.minFac = 1 by simp_all
    exact (le_antisymm (Nat.succ_le_of_lt lb) (Nat.lt_succ_iff.mp h')).symm

Похожие утверждения