translate — Mathlib

English

The action of translation by x on y yields x+y; i.e., translate by x applied to y equals x+y.

Русский

Действие трансляции на y на x даёт x+y: применив трансляцию на x к y получаем x+y.

LaTeX

$$@[simp] translate (Multiplicative.ofAdd x) y = x + y$$

Lean4

/-- The map `y ↦ x + y` as a `CircleDeg1Lift`. More precisely, we define a homomorphism from
`Multiplicative ℝ` to `CircleDeg1Liftˣ`, so the translation by `x` is
`translation (Multiplicative.ofAdd x)`. -/
def translate : Multiplicative ℝ →* CircleDeg1Liftˣ :=
  MonoidHom.toHomUnits <|
    { toFun := fun x => ⟨⟨fun y => x.toAdd + y, fun _ _ h => add_le_add_left h _⟩, fun _ => (add_assoc _ _ _).symm⟩
      map_one' := ext <| zero_add
      map_mul' := fun _ _ => ext <| add_assoc _ _ }

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