leftCoset_rightCoset — Mathlib

English

Equality of left and right coset interactions: op b • a • s = a • (op b • s).

Русский

Согласование левых и правых косетов: op b • a • s = a • (op b • s).

LaTeX

$$LeftCosetEquivalence(s, a, b) : (op b • a • s) = (a • (op b • s))$$

Lean4

@[to_additive leftAddCoset_rightAddCoset]
theorem leftCoset_rightCoset (s : Set α) (a b : α) : op b • a • s = a • (op b • s) := by
  simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

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