complexToReal — Mathlib

English

If E is a ℂ-star module, then E carries a natural ℝ-star module structure via restricting scalars, i.e., the star operation commutes with real scalar multiplication.

Русский

Если E — ℂ-Star-модуль, то E получает естественную ℝ-Star-структуру через ограничение скаляров: операция сопряжения коммутирует с вещественным умножением.

LaTeX

$$$ \forall r \in \mathbb{R}, \forall a \in E:\ \mathrm{star}(r \cdot a) = r \cdot \mathrm{star}(a). $$$

Lean4

instance (priority := 900) complexToReal {E : Type*} [AddCommGroup E] [Star E] [Module ℂ E] [StarModule ℂ E] :
    StarModule ℝ E :=
  ⟨fun r a => by rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]⟩

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