coe_intCast

Mathlib.Algebra.DirectSum.Internal

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

English

The integer embedding into A(0) agrees with the integer embedding into R, i.e., the natural casts coincide: (z : A(0)) = (z : R) for all z ∈ Z.

Русский

Целочисленное вложение в A(0) совпадает с вложением в R: для любого z ∈ Z выполняется (z : A_0) = (z : R).

LaTeX

$$(z : A_0) = (z : R) for all z ∈ \mathbb{Z}.$$

Lean4

theorem coe_intCast (z : ℤ) : (z : A 0) = (z : R) :=
  rfl

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

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

Разделы

Аффилиация

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