replicate_right_inj — Mathlib

English

For any a,b ∈ α and any n with n ≠ 0, replicate n a = replicate n b iff a = b.

Русский

Для любых a,b ∈ α и любого n ≠ 0 верно: replicate n a = replicate n b тогда и только если a = b.

LaTeX

$$$\\forall a,b : \\alpha,\\forall n : \\mathbb{N}, n \\neq 0 \\Rightarrow \\bigl( \\mathrm{replicate}(n,a) = \\mathrm{replicate}(n,b) \\iff a=b \\bigr).$$$

Lean4

theorem replicate_right_inj {a b : α} {n : ℕ} (h : n ≠ 0) : replicate n a = replicate n b ↔ a = b :=
  Subtype.ext_iff.trans (Multiset.replicate_right_inj h)

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