Documentation

Mathlib.Geometry.Manifold.Algebra.LieGroup

Lie groups #

A Lie group is a group that is also a smooth manifold, in which the group operations of multiplication and inversion are smooth maps. Smoothness of the group multiplication means that multiplication is a smooth mapping of the product manifold G × G into G.

Note that, since a manifold here is not second-countable and Hausdorff a Lie group here is not guaranteed to be second-countable (even though it can be proved it is Hausdorff). Note also that Lie groups here are not necessarily finite dimensional.

Main definitions #

Main results #

Implementation notes #

A priori, a Lie group here is a manifold with corners.

The definition of Lie group cannot require I : ModelWithCorners 𝕜 E E with the same space as the model space and as the model vector space, as one might hope, beause in the product situation, the model space is ModelProd E E' and the model vector space is E × E', which are not the same, so the definition does not apply. Hence the definition should be more general, allowing I : ModelWithCorners 𝕜 E H.

class LieAddGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [AddGroup G] [TopologicalSpace G] [ChartedSpace H G] extends SmoothAdd :

An additive Lie group is a group and a smooth manifold at the same time in which the addition and negation operations are smooth.

Instances
    theorem LieAddGroup.smooth_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [AddGroup G] [TopologicalSpace G] [ChartedSpace H G] [self : LieAddGroup I G] :
    Smooth I I fun (a : G) => -a

    Negation is smooth in an additive Lie group.

    class LieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [Group G] [TopologicalSpace G] [ChartedSpace H G] extends SmoothMul :

    A (multiplicative) Lie group is a group and a smooth manifold at the same time in which the multiplication and inverse operations are smooth.

    Instances
      theorem LieGroup.smooth_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Group G] [TopologicalSpace G] [ChartedSpace H G] [self : LieGroup I G] :
      Smooth I I fun (a : G) => a⁻¹

      Inversion is smooth in a Lie group.

      Smoothness of inversion, negation, division and subtraction #

      Let f : M → G be a C^n or smooth functions into a Lie group, then f is point-wise invertible with smooth inverse f. If f and g are two such functions, the quotient f / g (i.e., the point-wise product of f and the point-wise inverse of g) is also smooth.

      theorem smooth_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] :
      Smooth I I fun (x : G) => -x

      In an additive Lie group, inversion is a smooth map.

      theorem smooth_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] :
      Smooth I I fun (x : G) => x⁻¹

      In a Lie group, inversion is a smooth map.

      An additive Lie group is an additive topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

      theorem topologicalGroup_of_lieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] :

      A Lie group is a topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

      theorem ContMDiffWithinAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
      ContMDiffWithinAt I' I n (fun (x : M) => -f x) s x₀
      theorem ContMDiffWithinAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) :
      ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s x₀
      theorem ContMDiffAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
      ContMDiffAt I' I n (fun (x : M) => -f x) x₀
      theorem ContMDiffAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
      ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) x₀
      theorem ContMDiffOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) :
      ContMDiffOn I' I n (fun (x : M) => -f x) s
      theorem ContMDiffOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) :
      ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
      theorem ContMDiff.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} (hf : ContMDiff I' I n f) :
      ContMDiff I' I n fun (x : M) => -f x
      theorem ContMDiff.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} (hf : ContMDiff I' I n f) :
      ContMDiff I' I n fun (x : M) => (f x)⁻¹
      theorem SmoothWithinAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {s : Set M} {x₀ : M} (hf : SmoothWithinAt I' I f s x₀) :
      SmoothWithinAt I' I (fun (x : M) => -f x) s x₀
      theorem SmoothWithinAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {s : Set M} {x₀ : M} (hf : SmoothWithinAt I' I f s x₀) :
      SmoothWithinAt I' I (fun (x : M) => (f x)⁻¹) s x₀
      theorem SmoothAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {x₀ : M} (hf : SmoothAt I' I f x₀) :
      SmoothAt I' I (fun (x : M) => -f x) x₀
      theorem SmoothAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {x₀ : M} (hf : SmoothAt I' I f x₀) :
      SmoothAt I' I (fun (x : M) => (f x)⁻¹) x₀
      theorem SmoothOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {s : Set M} (hf : SmoothOn I' I f s) :
      SmoothOn I' I (fun (x : M) => -f x) s
      theorem SmoothOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {s : Set M} (hf : SmoothOn I' I f s) :
      SmoothOn I' I (fun (x : M) => (f x)⁻¹) s
      theorem Smooth.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} (hf : Smooth I' I f) :
      Smooth I' I fun (x : M) => -f x
      theorem Smooth.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} (hf : Smooth I' I f) :
      Smooth I' I fun (x : M) => (f x)⁻¹
      theorem ContMDiffWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
      ContMDiffWithinAt I' I n (fun (x : M) => f x - g x) s x₀
      theorem ContMDiffWithinAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
      ContMDiffWithinAt I' I n (fun (x : M) => f x / g x) s x₀
      theorem ContMDiffAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
      ContMDiffAt I' I n (fun (x : M) => f x - g x) x₀
      theorem ContMDiffAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) (hg : ContMDiffAt I' I n g x₀) :
      ContMDiffAt I' I n (fun (x : M) => f x / g x) x₀
      theorem ContMDiffOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
      ContMDiffOn I' I n (fun (x : M) => f x - g x) s
      theorem ContMDiffOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) :
      ContMDiffOn I' I n (fun (x : M) => f x / g x) s
      theorem ContMDiff.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      ContMDiff I' I n fun (x : M) => f x - g x
      theorem ContMDiff.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {g : MG} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      ContMDiff I' I n fun (x : M) => f x / g x
      theorem SmoothWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} {x₀ : M} (hf : SmoothWithinAt I' I f s x₀) (hg : SmoothWithinAt I' I g s x₀) :
      SmoothWithinAt I' I (fun (x : M) => f x - g x) s x₀
      theorem SmoothWithinAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} {x₀ : M} (hf : SmoothWithinAt I' I f s x₀) (hg : SmoothWithinAt I' I g s x₀) :
      SmoothWithinAt I' I (fun (x : M) => f x / g x) s x₀
      theorem SmoothAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {x₀ : M} (hf : SmoothAt I' I f x₀) (hg : SmoothAt I' I g x₀) :
      SmoothAt I' I (fun (x : M) => f x - g x) x₀
      theorem SmoothAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {x₀ : M} (hf : SmoothAt I' I f x₀) (hg : SmoothAt I' I g x₀) :
      SmoothAt I' I (fun (x : M) => f x / g x) x₀
      theorem SmoothOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} (hf : SmoothOn I' I f s) (hg : SmoothOn I' I g s) :
      SmoothOn I' I (f - g) s
      theorem SmoothOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} (hf : SmoothOn I' I f s) (hg : SmoothOn I' I g s) :
      SmoothOn I' I (f / g) s
      theorem Smooth.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} (hf : Smooth I' I f) (hg : Smooth I' I g) :
      Smooth I' I (f - g)
      theorem Smooth.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} (hf : Smooth I' I f) (hg : Smooth I' I g) :
      Smooth I' I (f / g)

      Binary product of Lie groups

      instance instLieAddGroupModelSumSumSum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [TopologicalSpace G'] [ChartedSpace H' G'] [AddGroup G'] [LieAddGroup I' G'] :
      LieAddGroup (I.prod I') (G × G')
      Equations
      • =
      instance instLieGroupModelProdProdProd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [TopologicalSpace G'] [ChartedSpace H' G'] [Group G'] [LieGroup I' G'] :
      LieGroup (I.prod I') (G × G')
      Equations
      • =

      Normed spaces are Lie groups #

      Equations
      • =

      Smooth manifolds with smooth inversion away from zero #

      Typeclass for smooth manifolds with 0 and Inv such that inversion is smooth at all non-zero points. (This includes multiplicative Lie groups, but also complete normed semifields.) Point-wise inversion is smooth when the function/denominator is non-zero.

      class SmoothInv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [Inv G] [Zero G] [TopologicalSpace G] [ChartedSpace H G] :

      A smooth manifold with 0 and Inv such that fun x ↦ x⁻¹ is smooth at all nonzero points. Any complete normed (semi)field has this property.

      • smoothAt_inv₀ : ∀ ⦃x : G⦄, x 0SmoothAt I I (fun (y : G) => y⁻¹) x

        Inversion is smooth away from 0.

      Instances
        theorem SmoothInv₀.smoothAt_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [Inv G] [Zero G] [TopologicalSpace G] [ChartedSpace H G] [self : SmoothInv₀ I G] ⦃x : G :
        x 0SmoothAt I I (fun (y : G) => y⁻¹) x

        Inversion is smooth away from 0.

        theorem smoothAt_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {x : G} (hx : x 0) :
        SmoothAt I I (fun (y : G) => y⁻¹) x

        In a manifold with smooth inverse away from 0, the inverse is continuous away from 0. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

        theorem SmoothOn_inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] :
        SmoothOn I I Inv.inv {0}
        theorem ContMDiffWithinAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {s : Set M} {a : M} (hf : ContMDiffWithinAt I' I n f s a) (ha : f a 0) :
        ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s a
        theorem ContMDiffAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {a : M} (hf : ContMDiffAt I' I n f a) (ha : f a 0) :
        ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) a
        theorem ContMDiff.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} (hf : ContMDiff I' I n f) (h0 : ∀ (x : M), f x 0) :
        ContMDiff I' I n fun (x : M) => (f x)⁻¹
        theorem ContMDiffOn.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : MG} {s : Set M} (hf : ContMDiffOn I' I n f s) (h0 : xs, f x 0) :
        ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
        theorem SmoothWithinAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {s : Set M} {a : M} (hf : SmoothWithinAt I' I f s a) (ha : f a 0) :
        SmoothWithinAt I' I (fun (x : M) => (f x)⁻¹) s a
        theorem SmoothAt.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {a : M} (hf : SmoothAt I' I f a) (ha : f a 0) :
        SmoothAt I' I (fun (x : M) => (f x)⁻¹) a
        theorem Smooth.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} (hf : Smooth I' I f) (h0 : ∀ (x : M), f x 0) :
        Smooth I' I fun (x : M) => (f x)⁻¹
        theorem SmoothOn.inv₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {s : Set M} (hf : SmoothOn I' I f s) (h0 : xs, f x 0) :
        SmoothOn I' I (fun (x : M) => (f x)⁻¹) s

        Point-wise division of smooth functions #

        If [SmoothMul I N] and [SmoothInv₀ I N], point-wise division of smooth functions f : M → N is smooth whenever the denominator is non-zero. (This includes N being a completely normed field.)

        theorem ContMDiffWithinAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} {a : M} {n : ℕ∞} (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a 0) :
        ContMDiffWithinAt I' I n (f / g) s a
        theorem ContMDiffOn.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) (h₀ : xs, g x 0) :
        ContMDiffOn I' I n (f / g) s
        theorem ContMDiffAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {a : M} {n : ℕ∞} (hf : ContMDiffAt I' I n f a) (hg : ContMDiffAt I' I n g a) (h₀ : g a 0) :
        ContMDiffAt I' I n (f / g) a
        theorem ContMDiff.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {n : ℕ∞} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ (x : M), g x 0) :
        ContMDiff I' I n (f / g)
        theorem SmoothWithinAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} {a : M} (hf : SmoothWithinAt I' I f s a) (hg : SmoothWithinAt I' I g s a) (h₀ : g a 0) :
        SmoothWithinAt I' I (f / g) s a
        theorem SmoothOn.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {s : Set M} (hf : SmoothOn I' I f s) (hg : SmoothOn I' I g s) (h₀ : xs, g x 0) :
        SmoothOn I' I (f / g) s
        theorem SmoothAt.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} {a : M} (hf : SmoothAt I' I f a) (hg : SmoothAt I' I g a) (h₀ : g a 0) :
        SmoothAt I' I (f / g) a
        theorem Smooth.div₀ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {f : MG} {g : MG} (hf : Smooth I' I f) (hg : Smooth I' I g) (h₀ : ∀ (x : M), g x 0) :
        Smooth I' I (f / g)