ofScientific_mem — Mathlib

English

Every number of the form OfScientific.ofScientific n b m, when viewed in K, lies in any subfield S of K; i.e., these numbers belong to all subfields.

Русский

Каждое число вида OfScientific.ofScientific n b m, рассмотренное как элемент K, принадлежит любому подполю S ⊆ K.

LaTeX

$$$\forall S:\text{Subfield } K, \forall n,m \in \mathbb{N}, \forall b \in \{0,1\}, (OfScientific.ofScientific n b m : K) \in S$$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem ofScientific_mem (s : S) {b : Bool} {n m : ℕ} : (OfScientific.ofScientific n b m : K) ∈ s :=
  SubfieldClass.nnratCast_mem s (OfScientific.ofScientific n b m)

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