instMul — Mathlib

English

Multiplication in 𝓜(𝕜, A) is defined so that the pair of its components is obtained by composing the first components and composing the second components in the opposite order: (a · b).toProd = (a.fst ∘ b.fst, b.snd ∘ a.snd).

Русский

Умножение в 𝓜(𝕜, A) задаётся так, чтобы пара компонент удовлетворяла (a·b).toProd = (a.fst ∘ b.fst, b.snd ∘ a.snd).

LaTeX

$$$ (a*b).toProd = (a.fst \circ b.fst,\; b.snd \circ a.snd)$$$

Lean4

instance instMul : Mul 𝓜(𝕜, A) where
  mul a
    b :=
    { toProd := (a.fst.comp b.fst, b.snd.comp a.snd)
      central := fun x y => show b.snd (a.snd x) * y = x * a.fst (b.fst y) by simp only [central] }

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