det_vandermonde_ne_zero_iff — Mathlib

English

For IsDomain R and v : Fin n → R, det(vandermonde v) ≠ 0 if and only if v is injective.

Русский

Для области R и v : Fin n → R, det(vandermonde v) ≠ 0 тогда и только если v инъективна.

LaTeX

$$$ \\det(\\mathrm{vandermonde} v) \\neq 0 \\iff \\mathrm{Function.Injective}\\, v. $$$

Lean4

theorem det_vandermonde_ne_zero_iff [IsDomain R] {v : Fin n → R} : det (vandermonde v) ≠ 0 ↔ Function.Injective v :=
  by
  unfold Function.Injective
  simp only [det_vandermonde_eq_zero_iff, Ne, not_exists, not_and, Classical.not_not]

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