sylvester_C_right — Mathlib

English

For any ring R, f ∈ R[X], m ∈ N, and a ∈ R, the Sylvester matrix of f and the constant C a at position m,0 is the diagonal matrix with a on the diagonal.

Русский

Для кольца R, f ∈ R[X], m ∈ N и a ∈ R матрица Сильвестра f и C a в позиции m,0 равна диагональной матрице с a на диагонали.

LaTeX

$$$\\text{Sylvester}(f,(C\\,a),m,0) = \\operatorname{Diagonal}(a)$$$

Lean4

@[simp]
theorem sylvester_C_right (a : R) : sylvester f (C a) m 0 = Matrix.diagonal (fun _ ↦ a) :=
  Matrix.ext fun i j ↦
    j.addCases nofun fun j ↦
      by
      rw [sylvester, Matrix.of_apply, Fin.addCases_right, Matrix.diagonal_apply]
      split_ifs <;> simp_all [Fin.ext_iff]

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