qsmul_mem — Mathlib

English

For S ⊆ K a subfield and x ∈ S, for any q ∈ ℚ, q • x ∈ S; i.e., S is closed under rational scalar multiplication.

Русский

Для подмножества S ⊆ K, являющегося подполем, при x ∈ S верно q • x ∈ S для любого q ∈ ℚ.

LaTeX

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

Lean4

@[aesop 90% (rule_sets := [SetLike])]
theorem qsmul_mem (s : S) (q : ℚ) (hx : x ∈ s) : q • x ∈ s := by
  simpa only [Rat.smul_def] using mul_mem (ratCast_mem _ _) hx

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