divLeft_eq_inv_trans_mulLeft — Mathlib

English

Let G be a group. For every a in G, the left-division by a is the same as first taking inverses and then left-multiplying by a; i.e. the left-division map by a equals the composition inv ∘ mulLeft(a).

Русский

Пусть G — группа. Для любого a∈G отображение слева на деление на a совпадает с применением сначала инверсии, затем левого умножения на a; то есть divLeft(a) = inv ∘ mulLeft(a).

LaTeX

$$$\\mathrm{divLeft}(a) = (\\mathrm{inv}\\;G) \\circ (\\mathrm{mulLeft}\\;a)$$$

Lean4

@[to_additive]
theorem divLeft_eq_inv_trans_mulLeft (a : G) : Equiv.divLeft a = (Equiv.inv G).trans (Equiv.mulLeft a) :=
  ext fun _ => div_eq_mul_inv _ _

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