inv_left

Mathlib.GroupTheory.RegularWreathProduct

URI: https://scilib.ai/kg/mathlib#RegularWreathProduct.inv_left

English

The left component of the inverse satisfies inv(d,f).left = (f)^{-1} applied to d^{-1}.

Русский

Левая часть обратного элемента удовлетворяет inv(d,f).left = f^{-1} · d^{-1}.

LaTeX

$$$\big( \operatorname{inv}(d,f) \big).\text{left} = (f)^{-1} \cdot d^{-1}.$$$

Lean4

@[simp]
theorem inv_left (a : D ≀ᵣ Q) : a⁻¹.left = fun x ↦ a.left⁻¹ (a.right * x) :=
  rfl

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

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

Разделы

Аффилиация

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