smul — Mathlib

English

Let f: 𝕜 → 𝕜 be meromorphic at x and g: 𝕜 → E be meromorphic at x. Then f • g is meromorphic at x.

Русский

Пусть f: 𝕜 → 𝕜 и g: 𝕜 → E — мероморфны в x. Тогда f z · g z мероморфна в x.

LaTeX

$$$MeromorphicAt f x \\to MeromorphicAt g x \\to MeromorphicAt (fun z \\mapsto f z \\cdot g z) x$$$

Lean4

@[fun_prop]
theorem smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    MeromorphicAt (f • g) x := by
  rcases hf with ⟨m, hf⟩
  rcases hg with ⟨n, hg⟩
  refine ⟨m + n, ?_⟩
  convert hf.fun_smul hg using 2 with z
  rw [Pi.smul_apply', smul_eq_mul]
  module

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