coe_nnqsmul — Mathlib

English

For q ∈ ℚ≥0 and a ∈ α with ha ≥ 0, ⟨q • a, proof⟩ = q • a in the ambient α sense.

Русский

Для q ∈ ℚ≥0 и a ∈ α с ha ≥ 0, соответствующий элемент ⟨q • a, …⟩ равен q • a в α-смысле.

LaTeX

$$$\\forall q \\in \\mathbb{Q}_{\\ge 0},\\; \\forall a, ha:\\; (\\langle q \\cdot a, ?\\rangle) = q \\cdot a$$$

Lean4

@[simp, norm_cast]
theorem coe_nnqsmul (q : ℚ≥0) (a : { x : α // 0 ≤ x }) : ↑(q • a) = (q • a : α) :=
  rfl

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