threeGPFree_smul_set — Mathlib

English

The GP-free property remains unchanged under scalar multiplication, i.e., ThreeGPFree(a•s) is equivalent to ThreeGPFree(s).

Русский

Свойство GP-free сохраняется при умножении множества на скаляр; ThreeGPFree(a•s) совпадает с ThreeGPFree(s).

LaTeX

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

Lean4

@[to_additive]
theorem threeGPFree_smul_set : ThreeGPFree (a • s) ↔ ThreeGPFree s
    where
  mp hs b hb c hc d hd
    h :=
    mul_left_cancel
      (hs (mem_image_of_mem _ hb) (mem_image_of_mem _ hc) (mem_image_of_mem _ hd) <| by
        rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h])
  mpr := ThreeGPFree.smul_set

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