no goals
F : Type ?u.17959
α : Type u_2
β : Type u_1
γ : Type ?u.17968
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
⊢ inducedMap α β 0 = 0
exact_mod_cast inducedMap_rat α β 0