op_smul_set_smul_eq_smul_smul_set

English

Under a compatibility condition h, the left-op-smul distributes across a bilinear product of sets: (op a • s) • t = s • a • t.

Русский

При условии совместимости h левая операция над OppSmul простирается на произведение множеств: (op a • s) • t = s • a • t.

LaTeX

$$$ (op a \cdot s) \cdot t = s \cdot a \cdot t $$$

Lean4

@[to_additive]
theorem op_smul_set_smul_eq_smul_smul_set (a : α) (s : Set β) (t : Set γ)
    (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_set, h]

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