lift_smul

Mathlib.Algebra.QuaternionBasis

URI: https://scilib.ai/kg/mathlib#QuaternionAlgebra.Basis.lift_smul

English

lift is compatible with scalar multiplication: lift(r • x) = r • lift(x).

Русский

lift совместим с умножением на скаляры: lift(r • x) = r • lift(x).

LaTeX

$$$\\text{lift}(r \\cdot x) = r \\cdot \\text{lift}(x)$$$

Lean4

theorem lift_smul (r : R) (x : ℍ[R,c₁,c₂,c₃]) : q.lift (r • x) = r • q.lift x := by
  simp [lift, mul_smul, ← Algebra.smul_def]

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

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

Разделы

Аффилиация

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