star_smul — Mathlib

English

The star operation fixes the image of the base ring under the algebra map: star (algebraMap r) = algebraMap r.

Русский

Звезда фиксирует образ элемента кольца через алгебраическое отображение: star (algebraMap r) = algebraMap r.

LaTeX

$$star (algebraMap R (CliffordAlgebra Q) r) = algebraMap R (CliffordAlgebra Q) r.$$

Lean4

/-- Note that this not match the `star_smul` implied by `StarModule`; it certainly could if we
also conjugated all the scalars, but there appears to be nothing in the literature that advocates
doing this. -/
@[simp]
theorem star_smul (r : R) (x : CliffordAlgebra Q) : star (r • x) = r • star x := by
  rw [star_def, star_def, map_smul, map_smul]

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