isHomogeneousElem_one

Mathlib.Algebra.GradedMonoid

URI: https://scilib.ai/kg/mathlib#SetLike.isHomogeneousElem_one

← MathLib Explorer

English

The unit element 1_R is homogeneous of degree 0 with respect to the grading A.

Русский

Единица 1_R однородна по градации и имеет степень 0.

LaTeX

$$$ 1_R \in A(0) $$$

Lean4

theorem isHomogeneousElem_one [Zero ι] [One R] (A : ι → S) [SetLike.GradedOne A] :
    SetLike.IsHomogeneousElem A (1 : R) :=
  ⟨0, SetLike.one_mem_graded _⟩

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

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

Разделы

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

Аффилиация

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