inv_smul_eq_iff — Mathlib

English

For a group action, g⁻¹ • a = b if and only if a = g • b.

Русский

Для группы: g⁻¹ • a = b тогда и только тогда, когда a = g • b.

LaTeX

$$$\\\\forall g \\\\in G, \\\\forall a \\\\in α, \\\\forall b \\\\in α, \\\\ g^{-1} \\\\cdot a = b \\\\iff \\\\ a = g \\\\cdot b.$$$

Lean4

@[to_additive]
theorem inv_smul_eq_iff : g⁻¹ • a = b ↔ a = g • b :=
  ⟨fun h ↦ by rw [← h, smul_inv_smul], fun h ↦ by rw [h, inv_smul_smul]⟩

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