det_mvPolynomialX_ne_zero — Mathlib

English

For a nontrivial ring, the determinant of mvPolynomialX is nonzero.

Русский

Для неабстрактной (несопоставимой) кольцевой структуры детерминант mvPolynomialX ненулевой.

LaTeX

$$$\det(\mathrm{mvPolynomialX}_{m m R}) \neq 0$$$

Lean4

/-- In a nontrivial ring, `Matrix.mvPolynomialX m m R` has non-zero determinant. -/
theorem det_mvPolynomialX_ne_zero [DecidableEq m] [Fintype m] [CommRing R] [Nontrivial R] :
    det (mvPolynomialX m m R) ≠ 0 := by
  intro h_det
  have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
  rw [det_one, ← RingHom.map_det, h_det, RingHom.map_zero] at this
  exact zero_ne_one this

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