eq_ratCast

Mathlib.Data.Rat.Cast.Defs

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

English

Given a ring hom from Rat to α, it maps any q ∈ Rat to q.cast in α.

Русский

Дано кольцевое отображение из Rat в α, оно отправляет любую q ∈ Rat в q.cast в α.

LaTeX

$$$\forall f:\, F \to Rat, \forall q:\, Rat,\ f q = q.cast.$$$

Lean4

@[simp]
theorem eq_ratCast [DivisionRing α] [FunLike F ℚ α] [RingHomClass F ℚ α] (f : F) (q : ℚ) : f q = q := by
  rw [← map_ratCast f, Rat.cast_id]

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

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

Разделы

Аффилиация

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