replicate_right_injective

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.replicate_right_injective

English

If n > 0, the map a ↦ replicate n a is injective.

Русский

Если n > 0, отображение a ↦ replicate n a инъективно.

LaTeX

$$$ n \\neq 0 \\Rightarrow \\operatorname{Injective}(\\lambda a : \\alpha, \\mathrm{replicate}(n,a)).$$$

Lean4

theorem replicate_right_injective {n : ℕ} (h : n ≠ 0) : Function.Injective (replicate n : α → Sym α n) := fun _ _ =>
  (replicate_right_inj h).1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru