smul_set₀ — Mathlib

English

GP-free is preserved under scalar multiplication; see 82804.

Русский

GP-free сохраняется при умножении множества на скаляр; см. 82804.

LaTeX

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

Lean4

theorem smul_set₀ (hs : ThreeGPFree s) (ha : a ≠ 0) : 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, ha] using h

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