instAddCommGroupWithOne

Mathlib.Algebra.QuadraticAlgebra

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

Lean4

instance : AddCommGroupWithOne (QuadraticAlgebra R a b)
    where
  intCast n := ((n : R) : QuadraticAlgebra R a b)
  intCast_ofNat n := by norm_cast
  intCast_negSucc n := by rw [Int.negSucc_eq, Int.cast_neg, coe_neg]; norm_cast

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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