self

Mathlib.Algebra.Central.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.IsCentral.self

English

The base ring K is central over itself: IsCentral K K holds.

Русский

Базис K является центральным относительно самого себя: IsCentral K K.

LaTeX

$$$\\mathrm{IsCentral}\\ K\\ K$$$

Lean4

instance self : IsCentral K K where out x := by simp [Algebra.mem_bot]

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

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

Разделы

Аффилиация

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