coe_replicate — Mathlib

English

The coercion of List.replicate to Multiset equals replicate: (List.replicate n a : Multiset α) = replicate n a.

Русский

Приведение List.replicate к Multiset совпадает с replicate: (List.replicate n a : Multiset α) = replicate n a.

LaTeX

$$$(\\text{List.replicate} \\; n \\; a : \\operatorname{Multiset} \\alpha) = \\operatorname{replicate}(n,a)$$$

Lean4

theorem coe_replicate (n : ℕ) (a : α) : (List.replicate n a : Multiset α) = replicate n a :=
  rfl

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