map_det

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

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

English

For a ring equivalence 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.mapMatrix M\big)$$$$

Lean4

theorem _root_.RingEquiv.map_det (f : R ≃+* S) (M : Matrix n n R) : f M.det = Matrix.det (f.mapMatrix M) :=
  f.toRingHom.map_det _

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

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

Разделы

Аффилиация

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