Theorems · Theorem · Lie groups

LeftInvariantDerivation.mk.inj

∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  {inst_4 : TopologicalSpace G} {inst_5 : ChartedSpace H G} {inst_6 : Monoid G} {inst_7 : ContMDiffMul I (↑⊤) G}
  {toDerivation :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)}
  {left_invariant'' :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation) = (Derivation.evalAt g) toDerivation}
  {toDerivation_1 :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)}
  {left_invariant''_1 :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation_1) = (Derivation.evalAt g) toDerivation_1},
  { toDerivation := toDerivation, left_invariant'' := left_invariant'' } =
      { toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 } →
    toDerivation = toDerivation_1

Defined in

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Cited by

1 results in Mathlib

Foundations

Depth 236 from the axioms · uses propext, Classical.choice, Quot.sound