single_mem_gradeBy

Mathlib.Algebra.MonoidAlgebra.Grading

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.single_mem_gradeBy

← MathLib Explorer

English

A single basis element δ_m r lies in the grade submodule at m.

Русский

Базисный элемент δ_m r принадлежит подмодулю степени m.

LaTeX

$$$\\mathsf{single}\\; m\\; r \\in \\text{gradeBy}(R,f)(f(m))$$$

Lean4

theorem single_mem_gradeBy {R} [CommSemiring R] (f : M → ι) (m : M) (r : R) : Finsupp.single m r ∈ gradeBy R f (f m) :=
  by
  intro x hx
  rw [Finset.mem_singleton.mp (Finsupp.support_single_subset hx)]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru