instNontrivial

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.instNontrivial

English

If α is nontrivial, then Sym2 α is nontrivial.

Русский

Если α ненулевой (есть два различных элемента), то Sym2 α ненулевой.

LaTeX

$$$[\\mathrm{Nontrivial}(\\alpha)] \\Rightarrow \\mathrm{Nontrivial}(\\mathrm{Sym}^2(\\alpha))$$$

Lean4

instance [Nontrivial α] : Nontrivial (Sym2 α) :=
  diag_injective.nontrivial

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

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

Разделы

Аффилиация

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