prime_of_factor — Mathlib

English

If x is in the factorization of a, then x is prime.

Русский

Если x встречается в разложении a, то x является простым.

LaTeX

$$$x \in \mathrm{factors}(a) \Rightarrow \mathrm{Prime}(x)$$$

Lean4

theorem prime_of_factor {a : α} (x : α) (hx : x ∈ factors a) : Prime x :=
  by
  have ane0 := ne_zero_of_mem_factors hx
  rw [factors, dif_neg ane0] at hx
  exact (Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 x hx

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