discr_smul

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.discr_smul

English

Discriminant scales predictably under scalar multiplication of the quadratic map.

Русский

Дискриминант корректно масштабируется при скалярном умножении квадратичной карты.

LaTeX

$$discr_smul (a) : (a • Q).discr = a^{|n|} discr(Q)$$

Lean4

theorem discr_smul (a : R) : (a • Q).discr = a ^ Fintype.card n * Q.discr := by
  simp only [discr, toMatrix'_smul, Matrix.det_smul]

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

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

Разделы

Аффилиация

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