isDiag_iff_proj_eq

Mathlib.Data.Sym.Sym2

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

English

For z ∈ α × α, IsDiag (Sym2.mk z) holds iff z.1 = z.2.

Русский

Для пары z = (z1, z2) из α × α утверждение IsDiag (Sym2.mk z) верно тогда и только тогда, когда z1 = z2.

LaTeX

$$$ \\text{IsDiag} (\\mathrm{Sym2.mk} z) \\iff z.1 = z.2. $$$

Lean4

@[simp]
theorem isDiag_iff_proj_eq (z : α × α) : IsDiag (Sym2.mk z) ↔ z.1 = z.2 :=
  Prod.recOn z fun _ _ => mk_isDiag_iff

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

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

Разделы

Аффилиация

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