coePNat_prime

Mathlib.Data.PNat.Factors

URI: https://scilib.ai/kg/mathlib#PrimeMultiset.coePNat_prime

← MathLib Explorer

English

If p ∈ v.toPNatMultiset for a prime multiset v, then p is prime.

Русский

Если p принадлежит v.toPNatMultiset, где v — PrimeMultiset, то p — простое.

LaTeX

$$coePNat_prime(v, p, h) : p ∈ v.toPNatMultiset → p.Prime$$

Lean4

theorem coePNat_prime (v : PrimeMultiset) (p : ℕ+) (h : p ∈ (v : Multiset ℕ+)) : p.Prime :=
  by
  rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru