coeFnRingHom — Mathlib

English

For a group-valued ContMDiffMap, taking the inverse corresponds to taking the pointwise inverse of the underlying function.

Русский

Обратное к отображению в пространстве ContMDiffMap даёт точечно обратное к соответствующей функции.

LaTeX

$$$\bigl(f^{-1}\bigr)(x)=f(x)^{-1} \quad (\forall x).$$$

Lean4

/-- Coercion to a function as a `RingHom`. -/
@[simps]
def coeFnRingHom {R : Type*} [CommRing R] [TopologicalSpace R] [ChartedSpace H' R] [ContMDiffRing I' n R] :
    C^n⟮I, N; I', R⟯ →+* N → R :=
  { (coeFnMonoidHom : C^n⟮I, N; I', R⟯ →* _), (coeFnAddMonoidHom : C^n⟮I, N; I', R⟯ →+ _) with toFun := (↑) }

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