restriction_of — Mathlib

English

For any p ∈ α, the restriction of the generator p to s is either the corresponding generator in FreeCommRing(s) if p ∈ s, or 0 if p ∉ s.

Русский

Для любого p ∈ α ограничение на генератор p в s равно соответствующему генератору в FreeCommRing(s), если p ∈ s, иначе 0.

LaTeX

$$$\\restriction_s(\\mathrm{of}(p)) = \\begin{cases} \\mathrm{of}\\langle p, H\\rangle, & p \\in s \\\\ 0, & p \\notin s \\end{cases}$$$

Lean4

@[simp]
theorem restriction_of (p) : restriction s (of p) = if H : p ∈ s then of ⟨p, H⟩ else 0 :=
  lift_of _ _

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