smul_coe

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

URI: https://scilib.ai/kg/mathlib#FixedDetMatrices.smul_coe

English

The coercion of the smul is the underlying multiplication on matrices.

Русский

Приведение к коэрценти smul совпадает с обычным умножением матриц.

LaTeX

$$$(instHSMul.hSMul g A).val = g \cdot A.1$$$

Lean4

theorem smul_coe (m : R) (g : SpecialLinearGroup n R) (A : FixedDetMatrix n R m) : (g • A).1 = g * A.1 := by
  rw [smul_def]

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

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

Разделы

Аффилиация

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