instCharZero

Mathlib.Algebra.Ring.Rat

URI: https://scilib.ai/kg/mathlib#Rat.instCharZero

← MathLib Explorer

English

The characteristic of ℚ is 0.

Русский

Характеристика ℚ равна 0.

LaTeX

$$$ \\text{CharZero } \\mathbb{Q}. $$$

Lean4

/-- The characteristic of `ℚ` is 0. -/
@[stacks 09FS "Second part."]
instance instCharZero : CharZero ℚ where cast_injective a b hab := by simpa using congr_arg num hab

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

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

Разделы

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

Аффилиация

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