@[deprecated algebraMap_mono (since := "2025-12-16")]

theorem algebraMap_monotone {α : Type u_1} (β : Type u_2) [CommSemiring α] [PartialOrder α] [Semiring β] [PartialOrder β] [IsOrderedRing β] [Algebra α β] [SMulPosMono α β] : Monotone ⇑(algebraMap α β)

Alias of algebraMap_mono.