eq_nnratCast

Mathlib.Data.Rat.Cast.Defs

URI: https://scilib.ai/kg/mathlib#eq_nnratCast

← MathLib Explorer

English

For a suitable F, q ∈ ℚ≥0 satisfies f q = q; equality holds in α.

Русский

Для подходящей функции f и q ∈ ℚ≥0 выполняется f q = q в α.

LaTeX

$$$\forall f:\, F, \forall q:\, \mathbb{Q}_{\ge 0},\ f q = q.$$$

Lean4

@[simp]
theorem eq_nnratCast [DivisionSemiring α] [FunLike F ℚ≥0 α] [RingHomClass F ℚ≥0 α] (f : F) (q : ℚ≥0) : f q = q := by
  rw [← map_nnratCast f, NNRat.cast_id]

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

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

Разделы

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

Аффилиация

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