isDiag_iff_mem_range_diag

Mathlib.Data.Sym.Sym2

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

English

An element z is diagonal if and only if z belongs to the range of diag.

Русский

Элемент z диагонален тогда и только тогда, когда он принадлежит образу diag.

LaTeX

$$$$ \IsDiag(z) \iff z \in \mathrm{range}(\mathrm{diag}). $$$$

Lean4

theorem isDiag_iff_mem_range_diag (z : Sym2 α) : IsDiag z ↔ z ∈ Set.range (@diag α) :=
  ⟨IsDiag.mem_range_diag, fun ⟨i, hi⟩ => hi ▸ diag_isDiag i⟩

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

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

Разделы

Аффилиация

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