smul_mem_smul_iff₀ — Mathlib

English

If a is nonzero in a group-with-zero, the smul equivalence holds as in the unit case.

Русский

Если a ≠ 0 в группе с нулём, эквивалентность сохраняется.

LaTeX

$$$ smul\\_mem\\_smul\\_iff\\_0 (ha : a \\neq 0) : a \\cdot p \\in a \\cdot s \\leftrightarrow p \\in s $$$

Lean4

theorem smul_mem_smul_iff₀ {G₀ : Type*} [GroupWithZero G₀] [DistribMulAction G₀ V] [SMulCommClass G₀ k V] {a : G₀}
    (ha : a ≠ 0) : a • p ∈ a • s ↔ p ∈ s :=
  smul_mem_smul_iff_of_isUnit ha.isUnit

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