mem_inv_pointwise_smul_iff — Mathlib

English

Let M be a group acting on the semiring R via a group action. If S is an ideal of R and a ∈ M, then for all x ∈ R, x ∈ a^{-1} • S if and only if a • x ∈ S.

Русский

Пусть M — группа, действующая на полукольцо R через групповое действие. Пусть S — идеал R и a ∈ M. Тогда для каждого x ∈ R верно: x ∈ a^{-1} • S тогда и только тогда a • x ∈ S.

LaTeX

$$$\forall a \in M\, \forall S \in \text{Ideal}(R)\, \forall x \in R:\ x \in a^{-1} \cdot S \ \iff\ a \cdot x \in S$$$

Lean4

theorem mem_inv_pointwise_smul_iff {a : M} {S : Ideal R} {x : R} : x ∈ a⁻¹ • S ↔ a • x ∈ S := by
  rw [mem_pointwise_smul_iff_inv_smul_mem, inv_inv]

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