nnqsmul_mem — Mathlib

English

If S is a subfield of K and x ∈ S, then for every q ∈ ℚ≥0, q • x ∈ S; i.e., S is closed under nonnegative rational scalar multiplication.

Русский

Если S — подполе K и x ∈ S, то для любого q ∈ ℚ≥0 верно q • x ∈ S; то есть S замкнуто относительно неотрицательного рационального умножения.

LaTeX

$$$x \in S \\\\Rightarrow q \\\\cdot x \in S \\\\text{ for all } q \\\\in \mathbb{Q}_{\\ge 0}$$$

Lean4

@[aesop 90% (rule_sets := [SetLike])]
theorem nnqsmul_mem (s : S) (q : ℚ≥0) (hx : x ∈ s) : q • x ∈ s := by
  simpa only [NNRat.smul_def] using mul_mem (nnratCast_mem _ _) hx

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