decidablePrime — Mathlib

Lean4
instance decidablePrime : DecidablePred PosNum.Prime
  | 1 => Decidable.isFalse Nat.not_prime_one
  | bit0 n =>
    decidable_of_iff' (n = 1)
      (by
        refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)
        · exact add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))
        rw [← minFac_to_nat, to_nat_inj]
        exact ⟨bit0.inj, congr_arg _⟩)
  | bit1 n =>
    decidable_of_iff' (minFacAux (bit1 n) n 1 = bit1 n) <|
      by
      refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)
      · simp only [cast_bit1]
        have := to_nat_pos n
        omega
      rw [← minFac_to_nat, to_nat_inj]; rfl
Похожие утверждения