English
For an algebra isomorphism f, the discriminant is preserved under composition with f on the basis: discr A (Matrix.vecMul b (P.map (...) )) = discr A b up to factor (det P)^2.
Русский
Дискриминант сохраняется при преобразовании через матричное умножение и изоморфизм: дискриминант через vecMul сохраняется до (det P)^2.
LaTeX
$$discr A (Matrix.vecMul b (P.map (algebraMap A B))) = P.det^2 * discr A b$$
Lean4
/-- Relation between `Algebra.discr A ι b` and
`Algebra.discr A ((P.map (algebraMap A B)) *ᵥ b)`. -/
theorem discr_of_matrix_mulVec (b : ι → B) (P : Matrix ι ι A) :
discr A (P.map (algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b := by
rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ← mul_assoc, discr_def,
pow_two]
