instNontrivialHAddNatOfNat

Mathlib.Data.Sym.Basic

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

English

If α is nontrivial, then Sym α (n+1) is nontrivial for every n.

Русский

Если α ненулевой, то Sym(α, n+1) ненулевой для любых n.

LaTeX

$$$\\operatorname{Nontrivial}(\\alpha) \\Rightarrow \\forall n, \\operatorname{Nontrivial}(\\mathrm{Sym}(\\alpha, n+1)).$$$

Lean4

instance (n : ℕ) [Nontrivial α] : Nontrivial (Sym α (n + 1)) :=
  (replicate_right_injective n.succ_ne_zero).nontrivial

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

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

Разделы

Аффилиация

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