inv — Mathlib

English

In a topological commutative group, inversion is a continuous monoid homomorphism E →* E.

Русский

Обратное в топологической группе непрерывно отображается как моноид-гомоморфизм E →* E.

LaTeX

$$$inv: \\text{ContinuousMonoidHom } E E$$$

Lean4

/-- The continuous homomorphism given by inversion. -/
@[to_additive (attr := simps!) /-- The continuous homomorphism given by negation. -/
    ]
def inv : ContinuousMonoidHom E E :=
  ⟨invMonoidHom, continuous_inv⟩

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