num_mem_deg

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

URI: https://scilib.ai/kg/mathlib#HomogeneousLocalization.num_mem_deg

English

The numerator of an element lies in the degree piece that is assigned to that element.

Русский

Числитель элемента лежит в той компоненте степени, которая назначена этому элементу.

LaTeX

$$$f.\\mathrm{num} \\in \\mathcal{A}_{f.\\deg}$$$

Lean4

theorem num_mem_deg (f : HomogeneousLocalization 𝒜 x) : f.num ∈ 𝒜 f.deg :=
  (Quotient.out f).num.2

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

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

Разделы

Аффилиация

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