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)