map_nnratCast — Mathlib

English

For any functor-like map from NNrat to α and q in ℚ≥0, the image equals q in α: f q = q.

Русский

Для любом отображения из NN Rat в α вернется тождественное отображение на q ∈ ℚ≥0: f q = q.

LaTeX

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

Lean4

@[simp]
theorem map_nnratCast [DivisionSemiring α] [DivisionSemiring β] [RingHomClass F α β] (f : F) (q : ℚ≥0) : f q = q := by
  simp_rw [NNRat.cast_def, map_div₀, map_natCast]

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