det — Mathlib

English

If every entry of a square matrix M over A is integral over R, then its determinant is integral over R.

Русский

Если каждая запись матрицы M интегральна над R, то детерминант M интегральен над R.

LaTeX

$$$\forall i,j, IsIntegral R (M_{ij}) \Rightarrow IsIntegral R (\det M)$$$

Lean4

theorem det {n : Type*} [Fintype n] [DecidableEq n] {M : Matrix n n A} (h : ∀ i j, IsIntegral R (M i j)) :
    IsIntegral R M.det := by
  rw [Matrix.det_apply]
  exact IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

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