mem_inv_smul_finset_iff₀ — Mathlib

English

If a ≠ 0 and s is a finite set of β, then b ∈ a^{-1} · s iff a · b ∈ s.

Русский

Если a ≠ 0 и s — конечное множество β, то b ∈ a^{-1} · s тогда и только если a · b ∈ s.

LaTeX

$$$a \neq 0 \implies (b \in a^{-1} \cdot s \;\iff\; a \cdot b \in s)$$$

Lean4

theorem mem_inv_smul_finset_iff₀ (ha : a ≠ 0) : b ∈ a⁻¹ • s ↔ a • b ∈ s :=
  show _ ∈ (Units.mk0 a ha)⁻¹ • _ ↔ _ from mem_inv_smul_finset_iff

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