English
Monotonicity of algebraMap: if a1 ≤ a2, then algebraMap a1 ≤ algebraMap a2.
Русский
Монотонность algebraMap: если a1 ≤ a2, то algebraMap a1 ≤ algebraMap a2.
LaTeX
$$$a_1 \le a_2 \Rightarrow \text{algebraMap } a_1 \le \text{algebraMap } a_2$$$
Lean4
@[simp]
theorem mk_smul (a : M) {k : K} (h : k ≠ 0) : mk (k • a) = mk a :=
by
have : Nontrivial K := nontrivial_iff.mpr ⟨k, 0, h⟩
obtain ⟨m, hm⟩ := Archimedean.arch 1 (show 0 < |k| by simpa using h)
obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)
simp_rw [mk_eq_mk, abs_smul]
refine ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩
· rw [← smul_assoc]
exact le_smul_of_one_le_left (by simp) hm
· have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]
rw [this]
exact smul_le_smul_of_nonneg_right hn (by simp)
