primeFactorsList_eq_nil — Mathlib

English

n.primeFactorsList = [] iff n = 0 or n = 1.

Русский

n.primeFactorsList = [] тогда и только тогда, когда n = 0 или n = 1.

LaTeX

$$$ n.primeFactorsList = [] \iff n = 0 \lor n = 1 $$$

Lean4

@[simp]
theorem primeFactorsList_eq_nil (n : ℕ) : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1 :=
  by
  constructor <;> intro h
  · rcases n with (_ | _ | n)
    · exact Or.inl rfl
    · exact Or.inr rfl
    · rw [primeFactorsList] at h
      injection h
  · rcases h with (rfl | rfl)
    · exact primeFactorsList_zero
    · exact primeFactorsList_one

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