instSMulProd — Mathlib

English

There is a natural action of D ≀ᵣ Q on Λ × Q given by w · (λ, q) = ((w.left (w.right · q)) · λ, w.right · q).

Русский

Существует естественное действие D ≀ᵣ Q на Λ × Q, заданное правилом w · (λ, q) = ((w.left (w.right · q)) · λ, w.right · q).

LaTeX

$$$ w \cdot (\lambda, q) = \left( (w.left (w.right \cdot q)) \cdot \lambda, \ w.right \cdot q \right) $$$

Lean4

instance : SMul (D ≀ᵣ Q) (Λ × Q) where smul w p := ⟨(w.left (w.right * p.2)) • p.1, w.right * p.2⟩

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