Repeating elements in multisets #
Main definitions #
replicate n a
is the multiset containing onlya
with multiplicityn
Alias of the reverse direction of Multiset.eq_replicate_card
.
theorem
Multiset.replicate_left_injective
{α : Type u_1}
(a : α)
:
Function.Injective fun (x : ℕ) => replicate x a
Multiplicity of an element #
@[simp]