smul_mem_smul_finset_iff₀ — Mathlib

English

A specialized equivalence for smul membership in a Finset space under a nontrivial scalar.

Русский

Специализированное равенство для членства во множестве Finset после скалярного умножения.

LaTeX

$$$\text{smul_mem_smul_finset}_0: \; (a \neq 0) \Rightarrow (a \cdot t) \ni (a \cdot b) \Leftrightarrow t \ni b$$$

Lean4

@[simp]
theorem smul_mem_smul_finset_iff₀ (ha : a ≠ 0) : a • b ∈ a • s ↔ b ∈ s :=
  smul_mem_smul_finset_iff (Units.mk0 a ha)

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