eq_inv_smul_iff — Mathlib

English

Equivalence form of inv_smul_iff: a = g⁻¹ • b if and only if g • a = b.

Русский

Эквивалентность inv_smul_iff: a = g⁻¹ • b ⇔ g • a = b.

LaTeX

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

Lean4

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

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