English
If M and N each carry OrderedSMul by 𝕜, then the product M × N also carries a natural coordinatewise OrderedSMul by 𝕜.
Русский
Если у M и N есть упорядоченное умножение 𝕜, то и произведение M × N имеет естественное координатное упорядочение умножения 𝕜.
LaTeX
$$$ OrderedSMul\ 𝕜\ (M \times N). $$$
Lean4
/-- To prove that a vector space over a linear ordered field is ordered, it suffices to verify only
the first axiom of `OrderedSMul`. -/
theorem mk' (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) : OrderedSMul 𝕜 M :=
by
have hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b :=
by
refine fun a b c hab hc => (h hab hc).lt_of_ne ?_
rw [Ne, hc.ne'.isUnit.smul_left_cancel]
exact hab.ne
refine ⟨fun {a b c} => hlt' a b c, fun {a b c hab hc} => ?_⟩
obtain ⟨c, rfl⟩ := hc.ne'.isUnit
rw [← inv_smul_smul c a, ← inv_smul_smul c b]
refine hlt' _ _ _ hab (pos_of_mul_pos_right ?_ hc.le)
simp only [c.mul_inv, zero_lt_one]
