map_det

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.map_det

← MathLib Explorer

English

For a ring hom f: R → S and M ∈ M_n(R), f(det M) = det(f.mapMatrix M).

Русский

Для кольцевого гомоморфа f: R → S и M ∈ M_n(R) выполняется f(det M) = det(f.mapMatrix M).

LaTeX

$$$$f(\det M) = \det\big(f(\mathrm{mapMatrix}(M))\big)$$$$

Lean4

theorem _root_.RingHom.map_det (f : R →+* S) (M : Matrix n n R) : f M.det = Matrix.det (f.mapMatrix M) := by
  simp [Matrix.det_apply', map_sum f, map_prod f]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru