discr_of_matrix_vecMul — Mathlib

English

Dual formula for discr with P.map and matrix multiplication on the left: discr A (P.map (algebraMap A B) *ᵥ b) = (det P)^2 · discr A b.

Русский

Двойная формула дискриминазации при умножении слева: дискриминант(P.map(…) *ᵥ b) = (det P)^2 · дискриминант(b).

LaTeX

$$discr A (P.map (RingHom.instFunLike.coe (algebraMap A B))).mulVec b) = (P.det)^2 * discr A b$$

Lean4

/-- Relation between `Algebra.discr A ι b` and
`Algebra.discr A (b ᵥ* P.map (algebraMap A B))`. -/
theorem discr_of_matrix_vecMul (b : ι → B) (P : Matrix ι ι A) :
    discr A (b ᵥ* P.map (algebraMap A B)) = P.det ^ 2 * discr A b := by
  rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ← mul_assoc, discr_def,
    pow_two]

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