leftMulMatrix — Mathlib

English

The matrix of left multiplication by pb.gen in the pb.basis is given by an explicit formula, matching pb.minpolyGen and pb.basis.

Русский

Матрица левого умножения на pb.gen в pb.basis задаётся явной формулой, согласующей pb.minpolyGen и pb.basis.

LaTeX

$$Algebra.leftMulMatrix pb.basis pb.gen = @Matrix.of (Fin pb.dim) (Fin pb.dim) _ (fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if (i : ℕ) = j + 1 then 1 else 0)$$

Lean4

protected theorem leftMulMatrix (pb : PowerBasis A S) :
    Algebra.leftMulMatrix pb.basis pb.gen =
      @Matrix.of (Fin pb.dim) (Fin pb.dim) _ fun i j =>
        if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if (i : ℕ) = j + 1 then 1 else 0 :=
  by
  cases subsingleton_or_nontrivial A; · subsingleton
  rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]
  refine pb.basis.ext fun k => ?_
  simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]
  apply (pow_succ' _ _).symm.trans
  split_ifs with h
  · simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]
    convert pb.aeval_minpolyGen
    rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff, pb.minpolyGen_monic.leadingCoeff, one_smul,
      natDegree_minpolyGen, Finset.sum_range]
  · rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]
    · rfl
    intro x hx
    rw [if_neg, zero_smul]
    apply mt Fin.ext hx

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