mem_range_diag

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.IsDiag.mem_range_diag

English

If z is diagonal, then z = diag x for some x.

Русский

Если z диагонален, то z = diag x для некоторого x.

LaTeX

$$$$ \forall z, \IsDiag(z) \to \exists x, z = \mathrm{diag}(x). $$$$

Lean4

theorem mem_range_diag {z : Sym2 α} : IsDiag z → z ∈ Set.range (@diag α) :=
  by
  obtain ⟨x, y⟩ := z
  rintro (rfl : x = y)
  exact ⟨_, rfl⟩

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

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

Разделы

Аффилиация

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