instFieldContMDiffRing — Mathlib

English

There is an induced ContMDiffMul structure, i.e., multiplication is smooth in the sense of ContMDiff, on ContMDiffRing.

Русский

Существует структура ContMDiffMul, т.е. умножение гладко в смысле ContMDiff, на ContMDiffRing.

LaTeX

$$$\\text{ContMDiffMul } I\,n\,R$$$

Lean4

instance (priority := 100) instFieldContMDiffRing {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} :
    ContMDiffRing 𝓘(𝕜) n 𝕜 :=
  { instNormedSpaceLieAddGroup with
    contMDiff_mul := by
      rw [contMDiff_iff]
      refine ⟨continuous_mul, fun x y => ?_⟩
      simp only [mfld_simps]
      rw [contDiffOn_univ]
      exact contDiff_mul }

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