English
The discriminant of the vecMul transformation of a vector family by a matrix P relates to the discriminant of the original family: discr A (b ᵥ* P.map (algebraMap A B)) = (det P)^2 · discr A b.
Русский
Дискриминант преобразования vecMul семейства вектора матрицей P связан с дискриминантом исходного семейства: дискриминант(меняем b через vecMul) = (det P)^2 · дискриминант(b).
LaTeX
$$discr A (Matrix.vecMul b (P.map (algebraMap A B))) = P.det^2 * discr A b$$
Lean4
/-- If `b` is not linear independent, then `Algebra.discr A b = 0`. -/
theorem discr_zero_of_not_linearIndependent [IsDomain A] {b : ι → B} (hli : ¬LinearIndependent A b) : discr A b = 0 :=
by
classical
obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
have : (traceMatrix A b) *ᵥ g = 0 := by
ext i
have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) :=
by
intro j
simp [mul_comm]
simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j => this j, ← map_sum,
← sum_mul, hg, zero_mul, LinearMap.map_zero]
by_contra h
rw [discr_def] at h
simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi
