smul_eq_zero_of_mem — Mathlib

English

If p lies in the kernel, then p acts on any cotangent element to yield zero.

Русский

Если p принадлежит ядру, то p действует на любой элемент котангенты, давая ноль.

LaTeX

$$$$ p \in P.ker \quad \Rightarrow \quad p \;\cdot\; m = 0 \text{ for all } m \in P.ker.Cotangent $$$$

Lean4

theorem smul_eq_zero_of_mem (p : P.Ring) (hp : p ∈ P.ker) (m : P.ker.Cotangent) : p • m = 0 :=
  Ideal.Cotangent.smul_eq_zero_of_mem hp m

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