inv_smul_mem_iff₀ — Mathlib

English

Let a act nontrivially (a ≠ 0) on β, and let s be a finite set of β. Then for any b ∈ β, a^{-1} · b ∈ s if and only if b ∈ a · s.

Русский

Пусть a действует на β с ненулевым значением (a ≠ 0). Пусть s — конечное множество элементов β. Тогда для любого b ∈ β верно: a^{-1} · b ∈ s тогда и только если b ∈ a · s.

LaTeX

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

Lean4

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

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