smul_set — Mathlib

English

If s is GP-free, then the scalar multiple a•s is GP-free as well.

Русский

Если s GP-free, то и масштабированное на скаляр множество a•s GP-free.

LaTeX

$$$ThreeGPFree(s) \Rightarrow ThreeGPFree(a\cdot s)$$$

Lean4

@[to_additive]
theorem smul_set (hs : ThreeGPFree s) : ThreeGPFree (a • s) :=
  by
  rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩ h
  exact congr_arg (a • ·) <| hs hb hc hd <| by simpa [mul_mul_mul_comm _ _ a] using h

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