grade_eq_lsingle_range

Mathlib.Algebra.MonoidAlgebra.Grading

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

English

The division by g yields the equality x = of'(g) · (x /ᵒᶠ g) + x %ᵒᶠ g.

Русский

Деление по g даёт равенство x = of'(g) · (x /ᵒᶠ g) + x %ᵒᶠ g.

LaTeX

$$$ x = \\operatorname{of}'(g) \\cdot (x /^{\\circ} g) + (x \\bmod^{\\circ} g) $$$

Lean4

theorem grade_eq_lsingle_range (m : M) : grade R m = LinearMap.range (Finsupp.lsingle m : R →ₗ[R] M →₀ R) :=
  Submodule.ext (mem_grade_iff' R m)

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

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

Разделы

Аффилиация

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