zero_mem — Mathlib

English

The action of R on p is defined by restricting the ambient action to p; in particular, for r ∈ R and x ∈ p, r • x ∈ p.

Русский

Действие R на p задаётся ограничением действием на M; для r ∈ R и x ∈ p имеем r • x ∈ p.

LaTeX

$$$ \\forall r \\in R, \\forall x \\in p:\\ r \\cdot x \\in p $$$

Lean4

theorem zero_mem (h : (p : Set M).Nonempty) : (0 : M) ∈ p :=
  let ⟨x, hx⟩ := h
  zero_smul R (x : M) ▸ p.smul_mem 0 hx

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