replicate_right_inj — Mathlib

English

For all a,b and n with n ≠ 0, replicate(n, a) = replicate(n, b) ⇔ a = b.

Русский

Для любых a,b и n с n ≠ 0: replicate(n, a) = replicate(n, b) эквивалентно a = b.

LaTeX

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

Lean4

theorem replicate_right_inj {a b : α} {n : ℕ} (hn : n ≠ 0) : replicate n a = replicate n b ↔ a = b :=
  (replicate_right_injective hn).eq_iff

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