op_smul_finset_smul_eq_smul_smul_finset

English

If h expresses the compatibility (op a • b) • c = b • a • c for all a, b, c, then applying op-smul to a Finset s and then smul-ing by t is the same as smul-ing by a and then smul-ing by t: (op a • s) • t = s • a • t.

Русский

Если задано соответствие (op a • b) • c = b • a • c для всех a, b, c, то применение обобщенного умножения к Finset s и далее умножение на t равно умножению на a и затем умножению на t: (op a • s) • t = s • a • t.

LaTeX

$$$\\forall a\\, s\\, t \\; (h : \\forall (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) \\Rightarrow (op a • s) • t = s • a • t$$$

Lean4

@[to_additive]
theorem op_smul_finset_smul_eq_smul_smul_finset (a : α) (s : Finset β) (t : Finset γ)
    (h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) : (op a • s) • t = s • a • t :=
  by
  ext
  simp [mem_smul, mem_smul_finset, h]

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