algebraMap_strictMono — Mathlib

English

The algebra map is strictly monotone: for a1 < a2, we have algebraMap a1 < algebraMap a2.

Русский

Отображение алгебра является строгим монотонным: если a1 < a2, то algebraMap a1 < algebraMap a2.

LaTeX

$$$a_1 < a_2 \Rightarrow \text{algebraMap } a_1 < \text{algebraMap } a_2$$$

Lean4

@[mono]
theorem algebraMap_strictMono : StrictMono (algebraMap α β) := fun a₁ a₂ ha ↦ by
  simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one

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