mul — Mathlib

English

An equivalence e : α ≃ β transfers multiplication from β to α by defining x*y := e^{-1}(e x · e y).

Русский

Эквивалентность e : α ≃ β переносит умножение с β на α через определение x*y := e^{-1}(e x · e y).

LaTeX

$$$$x\cdot y = e^{-1}( e x \cdot e y ).$$$$

Lean4

/-- Transfer `Mul` across an `Equiv` -/
@[to_additive /-- Transfer `Add` across an `Equiv` -/
    ]
protected abbrev mul [Mul β] : Mul α where mul x y := e.symm (e x * e y)

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