divRight_symm — Mathlib

English

The inverse of the right-division by c is the map mulRight c: (divRight c)^{-1} = mulRight c.

Русский

Обратная операция деления справа по c равна умножению справа на c: (divRight c)^{-1} = mulRight c.

LaTeX

$$$(\mathrm{divRight}\,c)^{-1} = \mathrm{mulRight}\,c$$$

Lean4

@[to_additive (attr := simp)]
theorem divRight_symm [IsIsometricSMul Gᵐᵒᵖ G] (c : G) : (divRight c).symm = mulRight c :=
  ext fun _ => rfl

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