mk_inv

Mathlib.Topology.Algebra.SeparationQuotient.Basic

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.mk_inv

English

mk preserves inverses: mk(x^{-1}) = (mk x)^{-1}.

Русский

mk сохраняет обратные элементы: mk(x^{-1}) = (mk x)^{-1}.

LaTeX

$$$\mathrm{mk\\_inv}: x \mapsto x^{-1} \Rightarrow \mathrm{mk}(x^{-1}) = (\mathrm{mk}x)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_inv [Inv G] [ContinuousInv G] (x : G) : mk x⁻¹ = (mk x)⁻¹ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru