Core

Mathlib.RingTheory.Extension.Presentation.Core

URI: https://scilib.ai/kg/mathlib#Algebra.Presentation.Core

English

The core subalgebra P.core is regarded as its own type; Core(P) is defined to be P.core.

Русский

Ядро подалгебры P.core рассматривается как свой тип; Core(P) задается как P.core.

LaTeX

$$$\mathrm{Core}(P) = P.core$$$

Lean4

/-- The core coerced to a type for performance reasons. -/
def Core : Type _ :=
  P.core

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

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

Разделы

Аффилиация

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