submonoid

Mathlib.Algebra.GradedMonoid

URI: https://scilib.ai/kg/mathlib#SetLike.GradeZero.submonoid

← MathLib Explorer

English

The unit 1 of R lies in A 0 when A defines a graded one.

Русский

Единица 1 из R принадлежит A 0, если определено градуированное единичное множество.

LaTeX

$$$1_R \\in A 0$$$

Lean4

/-- The submonoid `A 0` of `R`. -/
@[simps]
def submonoid : Submonoid R where
  carrier := A 0
  mul_mem' ha hb := add_zero (0 : ι) ▸ SetLike.mul_mem_graded ha hb
  one_mem' := SetLike.one_mem_graded A

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

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

Разделы

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

Аффилиация

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