cast_det — Mathlib

English

Let M ∈ M_n(ℤ). Then det(M) cast to an arbitrary ring R equals det of M with entries cast to R: (det M)^{R} = det(M^{R}).

Русский

Пусть M ∈ M_n(ℤ). Тогда det(M) при преобразовании в R равен det(M) с элементами, приведёнными к R: (det M)^{R} = det(M^{R}).

LaTeX

$$$$ (\det M : R) = \det\big(M\mapsto x \mapsto (x: R)\big) $$$$

Lean4

@[norm_cast]
theorem _root_.Int.cast_det (M : Matrix n n ℤ) : (M.det : R) = (M.map fun x ↦ (x : R)).det :=
  Int.castRingHom R |>.map_det M

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