disc_conj — Mathlib

English

The discriminant of a matrix is invariant under conjugation by GL(2): disc(g m g^{-1}) = disc(m).

Русский

Дискриминант матрицы инвариантен относительно сопряжения GL(2): disc(g m g^{-1}) = disc(m).

LaTeX

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

Lean4

@[simp]
theorem disc_conj : (g.val * m * g.val⁻¹).disc = m.disc := by
  simp only [disc_fin_two, ← Matrix.coe_units_inv, trace_units_conj, det_units_conj]

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