prod_ofPrime — Mathlib

English

The product of a one-element prime multiset equals that prime (as a positive naturals).

Русский

Произведение односоставного мультимножества, состоящего из простого p, равно этому простому p (как элемент ℕ+).

LaTeX

$$$ \\operatorname{prod}(\\operatorname{ofPrime}(p)) = p $$$

Lean4

theorem prod_ofPrime (p : Nat.Primes) : (ofPrime p).prod = (p : ℕ+) :=
  Multiset.prod_singleton _

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