inv_smul_mem_iff — Mathlib

English

An element lies in the inverse-smul translate a⁻¹ • s if and only if the original element lies in a • s.

Русский

Элемент принадлежит к перевернутой переноске: a⁻¹ • s, если и только если исходный элемент принадлежит a • s.

LaTeX

$$$a^{-1} \\cdot b \\in s \\iff b \\in a \\cdot s$$$

Lean4

@[to_additive]
theorem inv_smul_mem_iff : a⁻¹ • b ∈ s ↔ b ∈ a • s := by rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

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