coeNat_prime

Mathlib.Data.PNat.Factors

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

← MathLib Explorer

English

If p ∈ v.toNatMultiset for v a PrimeMultiset, then p is prime.

Русский

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

LaTeX

$$coeNat_prime(v, p, h) : p ∈ v.toNatMultiset → Nat.Prime p$$

Lean4

theorem coeNat_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