isDiag_mk_of_mem_diag

Mathlib.Data.Finset.Sym

URI: https://scilib.ai/kg/mathlib#Finset.isDiag_mk_of_mem_diag

English

If a ∈ s.diag, then (Sym2.mk a).IsDiag.

Русский

Если a ∈ s.diag, то (Sym2.mk a).IsDiag.

LaTeX

$$a \in s.diag \Rightarrow (Sym2.mk a).IsDiag$$

Lean4

theorem isDiag_mk_of_mem_diag {a : α × α} (h : a ∈ s.diag) : (Sym2.mk a).IsDiag :=
  (Sym2.isDiag_iff_proj_eq _).2 (mem_diag.1 h).2

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

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

Разделы

Аффилиация

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