mulRight — Mathlib

English

Right multiplication by a nonzero element a induces a dilation equivalence on a normed division ring.

Русский

Правое умножение на ненулевой элемент a индуцирует дилатационную эквивалентность на нормированном кольце деления.

LaTeX

$$$a \neq 0 \Rightarrow (x \mapsto x a) \text{ is a dilation-equivalence on the normed division ring } \alpha.$$$

Lean4

/-- Multiplication by a nonzero element `a` on the right
as a `DilationEquiv` of a normed division ring. -/
@[simps!]
def mulRight (a : α) (ha : a ≠ 0) : α ≃ᵈ α
    where
  __ := Dilation.mulRight a ha
  toEquiv := Equiv.mulRight₀ a ha

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