singleton_set_smul — Mathlib

English

For any r ∈ S, the set {r} acts on N by {r} • N = r • N.

Русский

Для любого r ∈ S множество {r} действует на N так, что {r}•N = r•N.

LaTeX

$$$ ({r} : Set S) \cdot N = r \cdot N $$$

Lean4

theorem singleton_set_smul [SMulCommClass S R M] (r : S) : ({ r } : Set S) • N = r • N :=
  by
  apply set_smul_eq_of_le
  · rintro _ m rfl hm; exact ⟨m, hm, rfl⟩
  · rintro _ ⟨m, hm, rfl⟩
    rw [mem_set_smul_def, Submodule.mem_sInf]
    intro _ hp; exact hp rfl hm

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