English
The standard part is multiplicative on finite hyperreals: st(x·y) = st(x)·st(y).
Русский
Стандартная часть сохраняет умножение для конечных гиперреальных: st(xy) = st(x)st(y).
LaTeX
$$$\\forall {x y : \\mathbb{R}^*}, \\neg Infinite x \\land \\neg Infinite y \\rightarrow st(x\\cdot y) = st(x) \\cdot st(y)$$$
Lean4
theorem st_mul {x y : ℝ*} (hx : ¬Infinite x) (hy : ¬Infinite y) : st (x * y) = st x * st y :=
have hx' := isSt_st' hx
have hy' := isSt_st' hy
have hxy := isSt_st' (not_infinite_mul hx hy)
hxy.unique (hx'.mul hy')