unitSMul — Mathlib

English

The action of units on the mixed space is a genuineMulAction: (uv) • x = u • (v • x).

Русский

Действие на смешанном пространстве является правильным действием умножения: (uv) • x = u • (v • x).

LaTeX

$$∀ u,v ∈ (𝓞 K)ˣ, ∀ x ∈ mixedSpace(K), (u v) • x = u • (v • x)$$

Lean4

/-- The action of `(𝓞 K)ˣ` on the mixed space `ℝ^r₁ × ℂ^r₂` defined, for `u : (𝓞 K)ˣ`, by
multiplication component by component with `mixedEmbedding K u`. -/
@[simps]
instance unitSMul : SMul (𝓞 K)ˣ (mixedSpace K) where smul u x := mixedEmbedding K u * x

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