top

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#Ideal.IsHomogeneous.top

English

The top (whole ring) is homogeneous with respect to any grading 𝒜.

Русский

Вся кольцо является однородным по отношению к любой градации 𝒜.

LaTeX

$$$\\text{Ideal.IsHomogeneous } 𝒜 \\; \\top$$$

Lean4

theorem top : Ideal.IsHomogeneous 𝒜 ⊤ := fun i r _ => by simp only [Submodule.mem_top]

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

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

Разделы

Аффилиация

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