cons_nonzero_iff

Mathlib.Algebra.Group.Fin.Tuple

URI: https://scilib.ai/kg/mathlib#Matrix.cons_nonzero_iff

← MathLib Explorer

English

vecCons x v is nonzero if and only if x ≠ 0 or v ≠ 0.

Русский

vecCons x v не ноль тогда и только если x ≠ 0 или v ≠ 0.

LaTeX

$$$ vecCons x v \neq 0 \iff x \neq 0 \lor v \neq 0 $$$

Lean4

theorem cons_nonzero_iff {v : Fin n → α} {x : α} : vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0
    where
  mp h := not_and_or.mp (h ∘ cons_eq_zero_iff.mpr)
  mpr h := mt cons_eq_zero_iff.mp (not_and_or.mpr h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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