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

• LieAddGroup I G : a Lie additive group where G is a manifold on the model with corners I.
• LieGroup I G : a Lie multiplicative group where G is a manifold on the model with corners I.
• SmoothInv₀: typeclass for smooth manifolds with 0 and Inv such that inversion is a smooth map at each non-zero point. This includes complete normed fields and (multiplicative) Lie groups.

Main results

• ContMDiff.inv, ContMDiff.div and variants: point-wise inversion and division of maps M → G is smooth
• ContMDiff.inv₀ and variants: if SmoothInv₀ N, point-wise inversion of smooth maps f : M → N is smooth at all points at which f doesn't vanish.
• ContMDiff.div₀ and variants: if also SmoothMul N (i.e., N is a Lie group except possibly for smoothness of inversion at 0), similar results hold for point-wise division.
• normedSpaceLieAddGroup : a normed vector space over a nontrivially normed field is an additive Lie group.
• Instances/UnitsOfNormedAlgebra shows that the group of units of a complete normed 𝕜-algebra is a multiplicative Lie group.

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, because 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 I G : Prop

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

• compatible : ∀ {e e' : PartialHomeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid (↑⊤) I
• smooth_add : ContMDiff (I.prod I) I ⊤ fun (p : G × G) => p.1 + p.2
• smooth_neg : ContMDiff 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 I G : Prop

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

• compatible : ∀ {e e' : PartialHomeomorph G H}, e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid (↑⊤) I
• smooth_mul : ContMDiff (I.prod I) I ⊤ fun (p : G × G) => p.1 * p.2
• smooth_inv : ContMDiff 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 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] [Group G] [LieGroup I G] : ContMDiff I I ⊤ fun (x : G) => x⁻¹

In a Lie group, inversion is a smooth map.

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_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] : ContMDiff I I ⊤ fun (x : G) => -x

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

@[deprecated contMDiff_inv]

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] [Group G] [LieGroup I G] : ContMDiff I I ⊤ fun (x : G) => x⁻¹

Alias of contMDiff_inv.

---

In a Lie group, inversion is a smooth map.

@[deprecated contMDiff_neg]

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_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] : ContMDiff I I ⊤ fun (x : G) => -x

Alias of contMDiff_neg.

---

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

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_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] : TopologicalGroup 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 topologicalAddGroup_of_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} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I G] : TopologicalAddGroup G

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 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] [Group G] [LieGroup 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 : M → G} {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.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} [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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} {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.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] [Group G] [LieGroup 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 : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) : ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) 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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) : ContMDiffAt I' I n (fun (x : M) => -f x) 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] [Group G] [LieGroup 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 : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => -f x) s

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] [Group G] [LieGroup 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 : M → G} (hf : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => (f x)⁻¹

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} (hf : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => -f x

@[deprecated ContMDiffWithinAt.inv]

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] [Group G] [LieGroup 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 : M → G} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) : ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s x₀

Alias of ContMDiffWithinAt.inv.

@[deprecated ContMDiffAt.inv]

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] [Group G] [LieGroup 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 : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) : ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) x₀

Alias of ContMDiffAt.inv.

@[deprecated ContMDiffOn.inv]

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] [Group G] [LieGroup 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 : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s

Alias of ContMDiffOn.inv.

@[deprecated ContMDiff.inv]

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] [Group G] [LieGroup 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 : M → G} (hf : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => (f x)⁻¹

Alias of ContMDiff.inv.

@[deprecated ContMDiffWithinAt.neg]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} {s : Set M} {x₀ : M} (hf : ContMDiffWithinAt I' I n f s x₀) : ContMDiffWithinAt I' I n (fun (x : M) => -f x) s x₀

Alias of ContMDiffWithinAt.neg.

@[deprecated ContMDiffAt.neg]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) : ContMDiffAt I' I n (fun (x : M) => -f x) x₀

Alias of ContMDiffAt.neg.

@[deprecated ContMDiffOn.neg]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) : ContMDiffOn I' I n (fun (x : M) => -f x) s

Alias of ContMDiffOn.neg.

@[deprecated ContMDiff.neg]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f : M → G} (hf : ContMDiff I' I n f) : ContMDiff I' I n fun (x : M) => -f x

Alias of ContMDiff.neg.

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] [Group G] [LieGroup 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 g : M → G} {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.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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} {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.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] [Group G] [LieGroup 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 g : M → G} {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.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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} {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.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] [Group G] [LieGroup 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 g : M → G} {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.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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} {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.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] [Group G] [LieGroup 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 g : M → G} (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.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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n fun (x : M) => f x - g x

@[deprecated ContMDiffWithinAt.div]

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] [Group G] [LieGroup 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 g : M → G} {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₀

Alias of ContMDiffWithinAt.div.

@[deprecated ContMDiffAt.div]

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] [Group G] [LieGroup 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 g : M → G} {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₀

Alias of ContMDiffAt.div.

@[deprecated ContMDiffOn.div]

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] [Group G] [LieGroup 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 g : M → G} {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

Alias of ContMDiffOn.div.

@[deprecated ContMDiff.div]

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] [Group G] [LieGroup 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 g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n fun (x : M) => f x / g x

Alias of ContMDiff.div.

@[deprecated ContMDiffWithinAt.sub]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} {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₀

Alias of ContMDiffWithinAt.sub.

@[deprecated ContMDiffAt.sub]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} {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₀

Alias of ContMDiffAt.sub.

@[deprecated ContMDiffOn.sub]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} {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

Alias of ContMDiffOn.sub.

@[deprecated ContMDiff.sub]

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_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'} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H' M] {n : ℕ∞} {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) : ContMDiff I' I n fun (x : M) => f x - g x

Alias of ContMDiff.sub.

Binary product of Lie groups

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

• ⋯ = ⋯

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

• ⋯ = ⋯

Normed spaces are Lie groups

instance normedSpaceLieAddGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : LieAddGroup (modelWithCornersSelf 𝕜 E) E

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] : Prop

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 ≠ 0 → ContMDiffAt I I ⊤ (fun (y : G) => y⁻¹) x

  Inversion is smooth away from 0.

instance instSmoothInv₀ModelWithCornersSelf {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : SmoothInv₀ (modelWithCornersSelf 𝕜 𝕜) 𝕜

Equations

• ⋯ = ⋯

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] {x : G} (hx : x ≠ 0) : ContMDiffAt I I ⊤ (fun (y : G) => y⁻¹) x

@[deprecated contMDiffAt_inv₀]

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) : ContMDiffAt I I ⊤ (fun (y : G) => y⁻¹) x

Alias of contMDiffAt_inv₀.

theorem hasContinuousInv₀_of_hasSmoothInv₀ {𝕜 : 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] : HasContinuousInv₀ G

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 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] : ContMDiffOn I I ⊤ Inv.inv {0}ᶜ

@[deprecated contMDiffOn_inv₀]

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] : ContMDiffOn I I ⊤ Inv.inv {0}ᶜ

Alias of contMDiffOn_inv₀.

@[deprecated contMDiffOn_inv₀]

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] : ContMDiffOn I I ⊤ Inv.inv {0}ᶜ

Alias of contMDiffOn_inv₀.

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 : M → G} {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 : M → G} {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 : M → G} (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 : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s

@[deprecated ContMDiffWithinAt.inv₀]

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] {n : ℕ∞} {f : M → G} {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

Alias of ContMDiffWithinAt.inv₀.

@[deprecated ContMDiffAt.inv₀]

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] {n : ℕ∞} {f : M → G} {a : M} (hf : ContMDiffAt I' I n f a) (ha : f a ≠ 0) : ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) a

Alias of ContMDiffAt.inv₀.

@[deprecated ContMDiffOn.inv₀]

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] {n : ℕ∞} {f : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s

Alias of ContMDiffOn.inv₀.

@[deprecated ContMDiff.inv₀]

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] {n : ℕ∞} {f : M → G} (hf : ContMDiff I' I n f) (h0 : ∀ (x : M), f x ≠ 0) : ContMDiff I' I n fun (x : M) => (f x)⁻¹

Alias of ContMDiff.inv₀.

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 g : M → G} {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 g : M → G} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) (h₀ : ∀ x ∈ s, 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 g : M → G} {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 g : M → G} {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)

@[deprecated ContMDiffWithinAt.div₀]

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 g : M → G} {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

Alias of ContMDiffWithinAt.div₀.

@[deprecated ContMDiffAt.div₀]

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 g : M → G} {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

Alias of ContMDiffAt.div₀.

@[deprecated ContMDiffOn.div₀]

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 g : M → G} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContMDiffOn I' I n (f / g) s

Alias of ContMDiffOn.div₀.

@[deprecated ContMDiff.div₀]

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 g : M → G} {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)

Alias of ContMDiff.div₀.