Theorems · Theorem · Lie groups

LeftInvariantDerivation.mk.injEq

∀ {𝕜 : 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

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceMonoidContMDiffMul