map_id — Mathlib

English

Let Q1 be a quadratic form on M1. The Clifford algebra homomorphism induced by the identity isometry on Q1 is the identity map on CliffordAlgebra Q1.

Русский

Пусть Q1 — квадратичная форма на M1. Гомоморфизм CliffordAlgebra, индуцируемый тождественным изометрическим отображением на Q1, является тождественным гомоморфизмом CliffordAlgebra Q1.

LaTeX

$$$ \mathrm{CliffordAlgebra.map}\bigl(\mathrm QuadraticMap.Isometry.id\, Q_1\bigr) = \mathrm{AlgHom.id}\, R\, (\mathrm{CliffordAlgebra} Q_1). $$$

Lean4

@[simp]
theorem map_id : map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁) := by ext m; exact map_apply_ι _ m

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