center_toNonUnitalSubsemiring

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.center_toNonUnitalSubsemiring

English

The center, when viewed as a nonunital subsemiring, matches the standard center notion for semirings.

Русский

Центр как ненулевой подполь semiring совпадает с каноном центра семиринга.

LaTeX

$$center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A$$

Lean4

@[simp]
theorem center_toNonUnitalSubsemiring : (center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A :=
  rfl

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

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

Разделы

Аффилиация

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