replicate_right_inj' — Mathlib

English

For all a,b and n, replicate(n, a) = replicate(n, b) iff n = 0 or a = b.

Русский

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

LaTeX

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

Lean4

theorem replicate_right_inj' {a b : α} : ∀ {n}, replicate n a = replicate n b ↔ n = 0 ∨ a = b
  | 0 => by simp
  | n + 1 => (replicate_right_inj n.succ_ne_zero).trans <| by simp only [n.succ_ne_zero, false_or]

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