num_neg

Mathlib.LinearAlgebra.Matrix.Integer

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

English

Taking the negative of a rational matrix negates its numerator: (-A).num = -A.num.

Русский

Отрицание матрицы приводит к отрицанию числителя: (-A).num = -A.num.

LaTeX

$$$$ (-A).\\mathrm{num} = -A.\\mathrm{num}. $$$$

Lean4

@[simp]
theorem num_neg (A : Matrix m n ℚ) : (-A).num = -A.num := by
  ext
  simp [Matrix.num]

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

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

Разделы

Аффилиация

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