coe_inv — Mathlib

English

For ring-valued C^n-maps, left-composition by a ring hom φ: R'→R'' together with a compatible ContMDiff φ, induces a ring homomorphism between the corresponding C^n-maps spaces: f ↦ φ∘f.

Русский

Для кольцевых C^n-отображений композиция слева по кольцом φ образует кольцевой гомоморфизм между пространствами отображений: f ↦ φ∘f.

LaTeX

$$$\text{If }φ:R'\to R''\text{ is a ring homomorphism and }hφ:\ ContMDiff I' I'' n φ,\;\; C^n(I,N; I',R')\to C^n(I,N; I'',R'')$ is a ring homomorphism.$$

Lean4

@[to_additive (attr := simp)]
theorem coe_inv {G : Type*} [Group G] [TopologicalSpace G] [ChartedSpace H' G] [LieGroup I' n G]
    (f : C^n⟮I, N; I', G⟯) : ⇑f⁻¹ = (⇑f)⁻¹ :=
  rfl

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