linearIndependent_aeval_val_pderiv_relation

English

The family { (aeval P.val) (pderiv (P.map j) (P.relation i)) } is linearly independent over S.

Русский

Семейство \\{ (aeval P.val)(pderiv(P.map j)(P.relation i)) \\} линейно независимо над S.

LaTeX

$$$\\text{linearIndependent}_S\\;\\big( i,j \\mapsto (\\mathrm{aeval}(P.val))(\\mathrm{pderiv}(P.map(j))(P.relation(i))) \\big)$$$

Lean4

theorem linearIndependent_aeval_val_pderiv_relation :
    LinearIndependent S (fun i j ↦ (aeval P.val) (pderiv (P.map j) (P.relation i))) :=
  by
  simp_rw [← SubmersivePresentation.basisDeriv_apply]
  exact P.basisDeriv.linearIndependent

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