of_intCast

Mathlib.Algebra.DirectSum.Ring

URI: https://scilib.ai/kg/mathlib#DirectSum.of_intCast

English

The direct sum at grade zero inherits a ring structure from the graded ring A via an injective mapping of A0 into the direct sum.

Русский

Прямая сумма на граде ноль наследует кольцевую структуру через внедрение A0 в прямую сумму.

LaTeX

$$Instance Ring (A 0)$$

Lean4

@[simp]
theorem of_intCast (n : ℤ) : of A 0 n = n := by rfl

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

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

Разделы

Аффилиация

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