English
n times a nonnegative element applied under the mk construction yields the corresponding nonnegative element with nsmul nonneg preserved.
Русский
Умножение неотрицательного элемента на натуральное число через конструктор mk сохраняет неотрицательность.
LaTeX
$$$n \\cdot ⟨x, hx⟩ = ⟨n \\cdot x, nsmul\_nonneg hx n⟩$$$
Lean4
@[simp]
theorem nsmul_mk [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) {x : α} (hx : 0 ≤ x) :
(n • (⟨x, hx⟩ : { x : α // 0 ≤ x })) = ⟨n • x, nsmul_nonneg hx n⟩ :=
rfl