mulLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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