threeGPFree_smul_set₀ — Mathlib

English

If a ≠ 0, GP-free is preserved under the nonzero scalar action: ThreeGPFree(a•s) ⇔ ThreeGPFree(s).

Русский

Если a ≠ 0, GP-free сохраняется при ненулевом скалярном действии: ThreeGPFree(a•s) ⇔ ThreeGPFree(s).

LaTeX

$$$a \neq 0 \Rightarrow (ThreeGPFree(a\cdot s) \iff ThreeGPFree(s))$$$

Lean4

theorem threeGPFree_smul_set₀ (ha : a ≠ 0) : ThreeGPFree (a • s) ↔ ThreeGPFree s :=
  ⟨fun hs b hb c hc d hd h ↦
    mul_left_cancel₀ ha
      (hs (Set.mem_image_of_mem _ hb) (Set.mem_image_of_mem _ hc) (Set.mem_image_of_mem _ hd) <| by
        rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]),
    fun hs => hs.smul_set₀ ha⟩

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