smul_mem_smul_iff — Mathlib

English

Let a ∈ A, s ∈ R, and r be a unit in R. Then r • s ∈ σ(r • a) if and only if s ∈ σ(a).

Русский

Пусть a ∈ A, s ∈ R и r — единица в R. Тогда r • s ∈ σ(r • a) тогда и только тогда, когда s ∈ σ(a).

LaTeX

$$$r \cdot s \in \sigma(r \cdot a) \iff s \in \sigma(a)$$$

Lean4

theorem smul_mem_smul_iff {a : A} {s : R} {r : Rˣ} : r • s ∈ σ (r • a) ↔ s ∈ σ a := by
  simp only [mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub, isUnit_smul_iff]

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