cast_det — Mathlib

English

For any field F of characteristic 0 and M ∈ M_n(ℚ), the image of det M in F equals the determinant of M with entries mapped into F.

Русский

Пусть F — поле характеристика 0 и M ∈ M_n(ℚ). Тогда det(M) в F равен det(M) с элементами, переводимыми в F.

LaTeX

$$$$ (\det M)^{F} = \det\big(M^{F}\big) $$$$

Lean4

@[norm_cast]
theorem _root_.Rat.cast_det {F : Type*} [Field F] [CharZero F] (M : Matrix n n ℚ) :
    (M.det : F) = (M.map fun x ↦ (x : F)).det :=
  Rat.castHom F |>.map_det M

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