disc_conj'

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

URI: https://scilib.ai/kg/mathlib#Matrix.disc_conj'

English

Conjugation by g^{-1} on m preserves the discriminant: disc(g^{-1} m g) = disc(m).

Русский

При сопряжении g^{-1} m g дискриминант сохраняется: disc(g^{-1} m g) = disc(m).

LaTeX

$$$\operatorname{disc}(g^{-1} m g) = \operatorname{disc}(m).$$$

Lean4

@[simp]
theorem disc_conj' : (g.val⁻¹ * m * g.val).disc = m.disc := by simpa using disc_conj g⁻¹

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

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

Разделы

Аффилиация

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