coe_intCast

Mathlib.Algebra.QuadraticAlgebra

URI: https://scilib.ai/kg/mathlib#QuadraticAlgebra.coe_intCast

English

The natural embedding of R into QuadraticAlgebra agrees with the integer cast: ↑(n : R) equals n in QuadraticAlgebra.

Русский

Единичное вложение R в QuadraticAlgebra согласуется с приведением к целым: ↑(n : R) равно n в QuadraticAlgebra.

LaTeX

$$$\uparrow(n:\,R) = (n:\,\text{QuadraticAlgebra})$$$

Lean4

@[norm_cast]
theorem coe_intCast (n : ℤ) : ↑(n : R) = (n : QuadraticAlgebra R a b) :=
  rfl

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

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

Разделы

Аффилиация

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