map_apply_ι

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.map_apply_ι

English

For an isometry f between Q1 and Q2 and any m in M1, applying map f to ι_Q1(m) yields ι_Q2(f(m)).

Русский

Для изометрии f между Q1 и Q2 и любого m ∈ M1, применение map f к ι_Q1(m) даёт ι_Q2(f(m)).

LaTeX

$$$\\mathrm{map} f (\\iota_{Q_1} (m)) = \\iota_{Q_2} (f(m))$$$

Lean4

@[simp]
theorem map_apply_ι (f : Q₁ →qᵢ Q₂) (m : M₁) : map f (ι Q₁ m) = ι Q₂ (f m) :=
  lift_ι_apply _ _ m

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

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

Разделы

Аффилиация

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