toLieAddGroup — Mathlib

English

Another instance asserting a LieAddGroup structure under a ContMDiffRing context, confirming the Lie group structure on the additive group of R.

Русский

Ещё один пример, устанавливающий структуру ЛиAddGroup на тождественной группе R в контексте ContMDiffRing.

LaTeX

$$$\\text{LieAddGroup}(I,n,R)$$$

Lean4

instance (priority := 100) toLieAddGroup (I : ModelWithCorners 𝕜 E H) (R : Type*) [Ring R] [TopologicalSpace R]
    [ChartedSpace H R] [ContMDiffRing I n R] : LieAddGroup I n R
    where
  compatible := StructureGroupoid.compatible (contDiffGroupoid n I)
  contMDiff_add := contMDiff_add I n
  contMDiff_neg := by simpa only [neg_one_mul] using contMDiff_mul_left (G := R) (a := -1)

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