Documentation

Mathlib.Geometry.Manifold.Algebra.Monoid

C^n monoid #

A C^n monoid is a monoid that is also a C^n manifold, in which multiplication is a C^n map of the product manifold G Γ— G into G.

In this file we define the basic structures to talk about C^n monoids: ContMDiffMul and its additive counterpart ContMDiffAdd. These structures are general enough to also talk about C^n semigroups.

class ContMDiffAdd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (G : Type u_4) [Add G] [TopologicalSpace G] [ChartedSpace H G] extends IsManifold I n G :

Basic hypothesis to talk about a C^n (Lie) additive monoid or a C^n additive semigroup. A C^n additive monoid over G, for example, is obtained by requiring both the instances AddMonoid G and ContMDiffAdd I n G.

Instances
    @[deprecated ContMDiffAdd (since := "2025-01-09")]
    def SmoothAdd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (G : Type u_4) [Add G] [TopologicalSpace G] [ChartedSpace H G] :

    Alias of ContMDiffAdd.


    Basic hypothesis to talk about a C^n (Lie) additive monoid or a C^n additive semigroup. A C^n additive monoid over G, for example, is obtained by requiring both the instances AddMonoid G and ContMDiffAdd I n G.

    Equations
    class ContMDiffMul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (G : Type u_4) [Mul G] [TopologicalSpace G] [ChartedSpace H G] extends IsManifold I n G :

    Basic hypothesis to talk about a C^n (Lie) monoid or a C^n semigroup. A C^n monoid over G, for example, is obtained by requiring both the instances Monoid G and ContMDiffMul I n G.

    Instances
      @[deprecated ContMDiffMul (since := "2025-01-09")]
      def SmoothMul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) (G : Type u_4) [Mul G] [TopologicalSpace G] [ChartedSpace H G] :

      Alias of ContMDiffMul.


      Basic hypothesis to talk about a C^n (Lie) monoid or a C^n semigroup. A C^n monoid over G, for example, is obtained by requiring both the instances Monoid G and ContMDiffMul I n G.

      Equations
      theorem ContMDiffMul.of_le {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] {m n : WithTop β„•βˆž} (hmn : m ≀ n) [h : ContMDiffMul I n G] :
      theorem ContMDiffAdd.of_le {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] {m n : WithTop β„•βˆž} (hmn : m ≀ n) [h : ContMDiffAdd I n G] :
      instance instContMDiffMulOfSomeENatTopOfLEInfty {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] {a : WithTop β„•βˆž} [ContMDiffMul I (β†‘βŠ€) G] [h : ENat.LEInfty a] :
      instance instContMDiffAddOfSomeENatTopOfLEInfty {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] {a : WithTop β„•βˆž} [ContMDiffAdd I (β†‘βŠ€) G] [h : ENat.LEInfty a] :
      instance instContMDiffMulOfTopWithTopENat {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] {a : WithTop β„•βˆž} [ContMDiffMul I ⊀ G] :
      instance instContMDiffAddOfTopWithTopENat {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] {a : WithTop β„•βˆž} [ContMDiffAdd I ⊀ G] :
      instance instContMDiffMulOfNatWithTopENatOfContinuousMul {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContinuousMul G] :
      instance instContMDiffAddOfNatWithTopENatOfContinuousAdd {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContinuousAdd G] :
      instance instContMDiffMulOfNatWithTopENat {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I 2 G] :
      instance instContMDiffAddOfNatWithTopENat {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I 2 G] :
      theorem contMDiff_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] :
      ContMDiff (I.prod I) I n fun (p : G Γ— G) => p.1 * p.2
      theorem contMDiff_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] :
      ContMDiff (I.prod I) I n fun (p : G Γ— G) => p.1 + p.2
      @[deprecated contMDiff_mul (since := "2024-11-20")]
      theorem smooth_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] :
      ContMDiff (I.prod I) I n fun (p : G Γ— G) => p.1 * p.2

      Alias of contMDiff_mul.

      @[deprecated contMDiff_add (since := "2024-11-20")]
      theorem smooth_add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] :
      ContMDiff (I.prod I) I n fun (p : G Γ— G) => p.1 + p.2

      Alias of contMDiff_add.

      theorem continuousMul_of_contMDiffMul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] :

      If the multiplication is C^n, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

      theorem continuousAdd_of_contMDiffAdd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] :

      If the addition is C^n, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

      @[deprecated continuousMul_of_contMDiffMul (since := "2025-01-09")]
      theorem continuousMul_of_smooth {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] (I : ModelWithCorners π•œ E H) (n : WithTop β„•βˆž) {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] :

      Alias of continuousMul_of_contMDiffMul.


      If the multiplication is C^n, then it is continuous. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].

      theorem ContMDiffWithinAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {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 (f * g) s x
      theorem ContMDiffWithinAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {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 (f + g) s x
      theorem ContMDiffAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M β†’ G} {x : M} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) :
      ContMDiffAt I' I n (f * g) x
      theorem ContMDiffAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M β†’ G} {x : M} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) :
      ContMDiffAt I' I n (f + g) x
      theorem ContMDiffOn.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {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 (f * g) s
      theorem ContMDiffOn.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {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 (f + g) s
      theorem ContMDiff.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M β†’ G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      ContMDiff I' I n (f * g)
      theorem ContMDiff.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M β†’ G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      ContMDiff I' I n (f + g)
      @[deprecated ContMDiffWithinAt.mul (since := "2024-11-21")]
      theorem SmoothWithinAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {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 (f * g) s x

      Alias of ContMDiffWithinAt.mul.

      @[deprecated ContMDiffAt.mul (since := "2024-11-21")]
      theorem SmoothAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M β†’ G} {x : M} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) :
      ContMDiffAt I' I n (f * g) x

      Alias of ContMDiffAt.mul.

      @[deprecated ContMDiffOn.mul (since := "2024-11-21")]
      theorem SmoothOn.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {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 (f * g) s

      Alias of ContMDiffOn.mul.

      @[deprecated ContMDiff.mul (since := "2024-11-21")]
      theorem Smooth.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffMul I n G] {f g : M β†’ G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      ContMDiff I' I n (f * g)

      Alias of ContMDiff.mul.

      @[deprecated ContMDiffWithinAt.add (since := "2024-11-21")]
      theorem SmoothWithinAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {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 (f + g) s x

      Alias of ContMDiffWithinAt.add.

      @[deprecated ContMDiffAt.add (since := "2024-11-21")]
      theorem SmoothAt.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M β†’ G} {x : M} (hf : ContMDiffAt I' I n f x) (hg : ContMDiffAt I' I n g x) :
      ContMDiffAt I' I n (f + g) x

      Alias of ContMDiffAt.add.

      @[deprecated ContMDiffOn.add (since := "2024-11-21")]
      theorem SmoothOn.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {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 (f + g) s

      Alias of ContMDiffOn.add.

      @[deprecated ContMDiff.add (since := "2024-11-21")]
      theorem Smooth.add {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H 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] [ContMDiffAdd I n G] {f g : M β†’ G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
      ContMDiff I' I n (f + g)

      Alias of ContMDiff.add.

      theorem contMDiff_mul_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a : G} :
      ContMDiff I I n fun (x : G) => a * x
      theorem contMDiff_add_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a : G} :
      ContMDiff I I n fun (x : G) => a + x
      @[deprecated contMDiff_mul_left (since := "2024-11-21")]
      theorem smooth_mul_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a : G} :
      ContMDiff I I n fun (x : G) => a * x

      Alias of contMDiff_mul_left.

      @[deprecated contMDiff_add_left (since := "2024-11-21")]
      theorem smooth_add_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a : G} :
      ContMDiff I I n fun (x : G) => a + x

      Alias of contMDiff_add_left.

      theorem contMDiffAt_mul_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a b : G} :
      ContMDiffAt I I n (fun (x : G) => a * x) b
      theorem contMDiffAt_add_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a b : G} :
      ContMDiffAt I I n (fun (x : G) => a + x) b
      theorem contMDiff_mul_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a : G} :
      ContMDiff I I n fun (x : G) => x * a
      theorem contMDiff_add_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a : G} :
      ContMDiff I I n fun (x : G) => x + a
      @[deprecated contMDiff_mul_right (since := "2024-11-21")]
      theorem smooth_mul_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a : G} :
      ContMDiff I I n fun (x : G) => x * a

      Alias of contMDiff_mul_right.

      @[deprecated contMDiff_add_right (since := "2024-11-21")]
      theorem smooth_add_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a : G} :
      ContMDiff I I n fun (x : G) => x + a

      Alias of contMDiff_add_right.

      theorem contMDiffAt_mul_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] {a b : G} :
      ContMDiffAt I I n (fun (x : G) => x * a) b
      theorem contMDiffAt_add_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {n : WithTop β„•βˆž} {G : Type u_4} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] {a b : G} :
      ContMDiffAt I I n (fun (x : G) => x + a) b
      theorem mdifferentiable_mul_left {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I 1 G] {a : G} :
      MDifferentiable I I fun (x : G) => a * x
      theorem mdifferentiable_add_left {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I 1 G] {a : G} :
      MDifferentiable I I fun (x : G) => a + x
      theorem mdifferentiableAt_mul_left {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I 1 G] {a b : G} :
      MDifferentiableAt I I (fun (x : G) => a * x) b
      theorem mdifferentiableAt_add_left {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I 1 G] {a b : G} :
      MDifferentiableAt I I (fun (x : G) => a + x) b
      theorem mdifferentiable_mul_right {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I 1 G] {a : G} :
      MDifferentiable I I fun (x : G) => x * a
      theorem mdifferentiable_add_right {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I 1 G] {a : G} :
      MDifferentiable I I fun (x : G) => x + a
      theorem mdifferentiableAt_mul_right {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I 1 G] {a b : G} :
      MDifferentiableAt I I (fun (x : G) => x * a) b
      theorem mdifferentiableAt_add_right {π•œ : 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} [Add G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I 1 G] {a b : G} :
      MDifferentiableAt I I (fun (x : G) => x + a) b
      def smoothLeftMul {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] (g : G) [ContMDiffMul I (β†‘βŠ€) G] :
      ContMDiffMap I I G G β†‘βŠ€

      Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑳. Lemmas involving smoothLeftMul with the notation 𝑳 usually use L instead of 𝑳 in the names.

      Equations
      def smoothRightMul {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] (g : G) [ContMDiffMul I (β†‘βŠ€) G] :
      ContMDiffMap I I G G β†‘βŠ€

      Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑹. Lemmas involving smoothRightMul with the notation 𝑹 usually use R instead of 𝑹 in the names.

      Equations

      Left multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑳. Lemmas involving smoothLeftMul with the notation 𝑳 usually use L instead of 𝑳 in the names.

      Equations

      Right multiplication by g. It is meant to mimic the usual notation in Lie groups. Used mostly through the notation 𝑹. Lemmas involving smoothRightMul with the notation 𝑹 usually use R instead of 𝑹 in the names.

      Equations
      @[simp]
      theorem L_apply {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] (g h : G) [ContMDiffMul I (β†‘βŠ€) G] :
      (smoothLeftMul I g) h = g * h
      @[simp]
      theorem R_apply {π•œ : 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} [Mul G] [TopologicalSpace G] [ChartedSpace H G] (g h : G) [ContMDiffMul I (β†‘βŠ€) G] :
      (smoothRightMul I g) h = h * g
      @[simp]
      theorem L_mul {π•œ : 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_8} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I (β†‘βŠ€) G] (g h : G) :
      @[simp]
      theorem R_mul {π•œ : 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_8} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I (β†‘βŠ€) G] (g h : G) :
      theorem smoothLeftMul_one {π•œ : 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_8} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H G'] [ContMDiffMul I (β†‘βŠ€) G'] (g' : G') :
      (smoothLeftMul I g') 1 = g'
      theorem smoothRightMul_one {π•œ : 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_8} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H G'] [ContMDiffMul I (β†‘βŠ€) G'] (g' : G') :
      (smoothRightMul I g') 1 = g'
      instance ContMDiffMul.prod {n : WithTop β„•βˆž} {π•œ : Type u_8} [NontriviallyNormedField π•œ] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_10} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (G : Type u_11) [TopologicalSpace G] [ChartedSpace H G] [Mul G] [ContMDiffMul I n G] {E' : Type u_12} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_13} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') (G' : Type u_14) [TopologicalSpace G'] [ChartedSpace H' G'] [Mul G'] [ContMDiffMul I' n G'] :
      ContMDiffMul (I.prod I') n (G Γ— G')
      instance ContMDiffAdd.prod {n : WithTop β„•βˆž} {π•œ : Type u_8} [NontriviallyNormedField π•œ] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace π•œ E] {H : Type u_10} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) (G : Type u_11) [TopologicalSpace G] [ChartedSpace H G] [Add G] [ContMDiffAdd I n G] {E' : Type u_12} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {H' : Type u_13} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') (G' : Type u_14) [TopologicalSpace G'] [ChartedSpace H' G'] [Add G'] [ContMDiffAdd I' n G'] :
      ContMDiffAdd (I.prod I') n (G Γ— G')
      theorem contMDiff_pow {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] (i : β„•) :
      ContMDiff I I n fun (a : G) => a ^ i
      theorem contMDiff_nsmul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] (i : β„•) :
      ContMDiff I I n fun (a : G) => i β€’ a
      @[deprecated contMDiff_pow (since := "2024-11-21")]
      theorem smooth_pow {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n G] (i : β„•) :
      ContMDiff I I n fun (a : G) => a ^ i

      Alias of contMDiff_pow.

      @[deprecated contMDiff_nsmul (since := "2024-11-21")]
      theorem smooth_nsmul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n G] (i : β„•) :
      ContMDiff I I n fun (a : G) => i β€’ a

      Alias of contMDiff_nsmul.

      structure ContMDiffAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] (I : ModelWithCorners π•œ E H) (I' : ModelWithCorners π•œ E' H') (n : WithTop β„•βˆž) (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [AddMonoid G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [AddMonoid G'] extends G β†’+ G' :
      Type (max u_8 u_9)

      Morphism of additive C^n monoids.

      @[deprecated ContMDiffAddMonoidMorphism (since := "2025-01-09")]
      def SmoothAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] (I : ModelWithCorners π•œ E H) (I' : ModelWithCorners π•œ E' H') (n : WithTop β„•βˆž) (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [AddMonoid G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [AddMonoid G'] :
      Type (max u_8 u_9)

      Alias of ContMDiffAddMonoidMorphism.


      Morphism of additive C^n monoids.

      Equations
      structure ContMDiffMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] (I : ModelWithCorners π•œ E H) (I' : ModelWithCorners π•œ E' H') (n : WithTop β„•βˆž) (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [Monoid G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [Monoid G'] extends G β†’* G' :
      Type (max u_8 u_9)

      Morphism of C^n monoids.

      @[deprecated ContMDiffMonoidMorphism (since := "2025-01-09")]
      def SmoothMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] (I : ModelWithCorners π•œ E H) (I' : ModelWithCorners π•œ E' H') (n : WithTop β„•βˆž) (G : Type u_8) [TopologicalSpace G] [ChartedSpace H G] [Monoid G] (G' : Type u_9) [TopologicalSpace G'] [ChartedSpace H' G'] [Monoid G'] :
      Type (max u_8 u_9)

      Alias of ContMDiffMonoidMorphism.


      Morphism of C^n monoids.

      Equations
      instance instOneContMDiffMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      Equations
      instance instZeroContMDiffAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      Equations
      instance instInhabitedContMDiffMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      Equations
      instance instInhabitedContMDiffAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      Equations
      instance instFunLikeContMDiffMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      FunLike (ContMDiffMonoidMorphism I I' n G G') G G'
      Equations
      instance instFunLikeContMDiffAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      Equations
      instance instMonoidHomClassContMDiffMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      instance instAddMonoidHomClassContMDiffAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      instance instContinuousMapClassContMDiffMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [Monoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :
      instance instContinuousMapClassContMDiffAddMonoidMorphism {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [AddMonoid G] [TopologicalSpace G] [ChartedSpace H G] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace π•œ E'] {I' : ModelWithCorners π•œ E' H'} {G' : Type u_7} [AddMonoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] :

      Differentiability of finite point-wise sums and products #

      Finite point-wise products (resp. sums) of C^n functions M β†’ G (at x/on s) into a commutative monoid G are C^n at x/on s.

      theorem ContMDiffWithinAt.prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {xβ‚€ : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s xβ‚€) :
      ContMDiffWithinAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) s xβ‚€
      theorem ContMDiffWithinAt.sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {xβ‚€ : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s xβ‚€) :
      ContMDiffWithinAt I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) s xβ‚€
      theorem contMDiffWithinAt_finprod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) {xβ‚€ : M} (h : βˆ€ (i : ΞΉ), ContMDiffWithinAt I' I n (f i) s xβ‚€) :
      ContMDiffWithinAt I' I n (fun (x : M) => ∏ᢠ (i : ΞΉ), f i x) s xβ‚€
      theorem contMDiffWithinAt_finsum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) {xβ‚€ : M} (h : βˆ€ (i : ΞΉ), ContMDiffWithinAt I' I n (f i) s xβ‚€) :
      ContMDiffWithinAt I' I n (fun (x : M) => βˆ‘αΆ  (i : ΞΉ), f i x) s xβ‚€
      theorem contMDiffWithinAt_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x
      theorem contMDiffWithinAt_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (βˆ‘ i ∈ t, f i) s x
      theorem contMDiffWithinAt_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) s x
      theorem contMDiffWithinAt_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) s x
      theorem ContMDiffAt.prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {xβ‚€ : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) xβ‚€) :
      ContMDiffAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) xβ‚€
      theorem ContMDiffAt.sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {xβ‚€ : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) xβ‚€) :
      ContMDiffAt I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) xβ‚€
      theorem contMDiffAt_finprod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {xβ‚€ : M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) (h : βˆ€ (i : ΞΉ), ContMDiffAt I' I n (f i) xβ‚€) :
      ContMDiffAt I' I n (fun (x : M) => ∏ᢠ (i : ΞΉ), f i x) xβ‚€
      theorem contMDiffAt_finsum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {xβ‚€ : M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) (h : βˆ€ (i : ΞΉ), ContMDiffAt I' I n (f i) xβ‚€) :
      ContMDiffAt I' I n (fun (x : M) => βˆ‘αΆ  (i : ΞΉ), f i x) xβ‚€
      theorem contMDiffAt_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (∏ i ∈ t, f i) x
      theorem contMDiffAt_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (βˆ‘ i ∈ t, f i) x
      theorem contMDiffAt_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) x
      theorem contMDiffAt_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) x
      theorem contMDiffOn_finprod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) (h : βˆ€ (i : ΞΉ), ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (fun (x : M) => ∏ᢠ (i : ι), f i x) s
      theorem contMDiffOn_finsum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) (h : βˆ€ (i : ΞΉ), ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (fun (x : M) => βˆ‘αΆ  (i : ΞΉ), f i x) s
      theorem contMDiffOn_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (∏ i ∈ t, f i) s
      theorem contMDiffOn_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (βˆ‘ i ∈ t, f i) s
      theorem contMDiffOn_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (fun (x : M) => ∏ i ∈ t, f i x) s
      theorem contMDiffOn_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) s
      theorem ContMDiff.prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ i ∈ t, f i x
      theorem ContMDiff.sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘ i ∈ t, f i x
      theorem contMDiff_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n (∏ i ∈ t, f i)
      theorem contMDiff_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n (βˆ‘ i ∈ t, f i)
      theorem contMDiff_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ i ∈ t, f i x
      theorem contMDiff_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘ i ∈ t, f i x
      theorem contMDiff_finprod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : ΞΉ β†’ M β†’ G} (h : βˆ€ (i : ΞΉ), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ᢠ (i : ι), f i x
      theorem contMDiff_finsum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : ΞΉ β†’ M β†’ G} (h : βˆ€ (i : ΞΉ), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘αΆ  (i : ΞΉ), f i x
      theorem contMDiff_finprod_cond {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : ΞΉ β†’ M β†’ G} {p : ΞΉ β†’ Prop} (hc : βˆ€ (i : ΞΉ), p i β†’ ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ᢠ (i : ι) (_ : p i), f i x
      theorem contMDiff_finsum_cond {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : ΞΉ β†’ M β†’ G} {p : ΞΉ β†’ Prop} (hc : βˆ€ (i : ΞΉ), p i β†’ ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘αΆ  (i : ΞΉ) (_ : p i), f i x
      @[deprecated contMDiffAt_finprod (since := "2024-11-21")]
      theorem smoothAt_finprod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {xβ‚€ : M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) (h : βˆ€ (i : ΞΉ), ContMDiffAt I' I n (f i) xβ‚€) :
      ContMDiffAt I' I n (fun (x : M) => ∏ᢠ (i : ΞΉ), f i x) xβ‚€

      Alias of contMDiffAt_finprod.

      @[deprecated contMDiffAt_finsum (since := "2024-11-21")]
      theorem smoothAt_finsum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {xβ‚€ : M} {f : ΞΉ β†’ M β†’ G} (lf : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) (h : βˆ€ (i : ΞΉ), ContMDiffAt I' I n (f i) xβ‚€) :
      ContMDiffAt I' I n (fun (x : M) => βˆ‘αΆ  (i : ΞΉ), f i x) xβ‚€

      Alias of contMDiffAt_finsum.

      @[deprecated contMDiffWithinAt_finset_prod' (since := "2024-11-21")]
      theorem smoothWithinAt_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x

      Alias of contMDiffWithinAt_finset_prod'.

      @[deprecated contMDiffWithinAt_finset_sum' (since := "2024-11-21")]
      theorem smoothWithinAt_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (βˆ‘ i ∈ t, f i) s x

      Alias of contMDiffWithinAt_finset_sum'.

      @[deprecated contMDiffWithinAt_finset_prod (since := "2024-11-21")]
      theorem smoothWithinAt_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) s x

      Alias of contMDiffWithinAt_finset_prod.

      @[deprecated contMDiffWithinAt_finset_sum (since := "2024-11-21")]
      theorem smoothWithinAt_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) s x

      Alias of contMDiffWithinAt_finset_sum.

      @[deprecated contMDiffAt_finset_prod' (since := "2024-11-21")]
      theorem smoothAt_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (∏ i ∈ t, f i) x

      Alias of contMDiffAt_finset_prod'.

      @[deprecated contMDiffAt_finset_sum' (since := "2024-11-21")]
      theorem smoothAt_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (βˆ‘ i ∈ t, f i) x

      Alias of contMDiffAt_finset_sum'.

      @[deprecated contMDiffAt_finset_prod (since := "2024-11-21")]
      theorem smoothAt_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (fun (x : M) => ∏ i ∈ t, f i x) x

      Alias of contMDiffAt_finset_prod.

      @[deprecated contMDiffAt_finset_sum (since := "2024-11-21")]
      theorem smoothAt_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {x : M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffAt I' I n (f i) x) :
      ContMDiffAt I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) x

      Alias of contMDiffAt_finset_sum.

      @[deprecated contMDiffOn_finset_prod' (since := "2024-11-21")]
      theorem smoothOn_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (∏ i ∈ t, f i) s

      Alias of contMDiffOn_finset_prod'.

      @[deprecated contMDiffOn_finset_sum' (since := "2024-11-21")]
      theorem smoothOn_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (βˆ‘ i ∈ t, f i) s

      Alias of contMDiffOn_finset_sum'.

      @[deprecated contMDiffOn_finset_prod (since := "2024-11-21")]
      theorem smoothOn_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (fun (x : M) => ∏ i ∈ t, f i x) s

      Alias of contMDiffOn_finset_prod.

      @[deprecated contMDiffOn_finset_sum (since := "2024-11-21")]
      theorem smoothOn_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (fun (x : M) => βˆ‘ i ∈ t, f i x) s

      Alias of contMDiffOn_finset_sum.

      @[deprecated contMDiffOn_finset_prod' (since := "2024-11-21")]
      theorem smooth_finset_prod' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (∏ i ∈ t, f i) s

      Alias of contMDiffOn_finset_prod'.

      @[deprecated contMDiffOn_finset_sum' (since := "2024-11-21")]
      theorem smooth_finset_sum' {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {s : Set M} {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiffOn I' I n (f i) s) :
      ContMDiffOn I' I n (βˆ‘ i ∈ t, f i) s

      Alias of contMDiffOn_finset_sum'.

      @[deprecated contMDiff_finset_prod (since := "2024-11-21")]
      theorem smooth_finset_prod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ i ∈ t, f i x

      Alias of contMDiff_finset_prod.

      @[deprecated contMDiff_finset_sum (since := "2024-11-21")]
      theorem smooth_finset_sum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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] {t : Finset ΞΉ} {f : ΞΉ β†’ M β†’ G} (h : βˆ€ i ∈ t, ContMDiff I' I n (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘ i ∈ t, f i x

      Alias of contMDiff_finset_sum.

      @[deprecated contMDiff_finprod (since := "2024-11-21")]
      theorem smooth_finprod {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : ΞΉ β†’ M β†’ G} (h : βˆ€ (i : ΞΉ), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ᢠ (i : ι), f i x

      Alias of contMDiff_finprod.

      @[deprecated contMDiff_finsum (since := "2024-11-21")]
      theorem smooth_finsum {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : ΞΉ β†’ M β†’ G} (h : βˆ€ (i : ΞΉ), ContMDiff I' I n (f i)) (hfin : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘αΆ  (i : ΞΉ), f i x

      Alias of contMDiff_finsum.

      @[deprecated contMDiff_finprod_cond (since := "2024-11-21")]
      theorem smooth_finprod_cond {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : ΞΉ β†’ M β†’ G} {p : ΞΉ β†’ Prop} (hc : βˆ€ (i : ΞΉ), p i β†’ ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ΞΉ) => Function.mulSupport (f i)) :
      ContMDiff I' I n fun (x : M) => ∏ᢠ (i : ι) (_ : p i), f i x

      Alias of contMDiff_finprod_cond.

      @[deprecated contMDiff_finsum_cond (since := "2024-11-21")]
      theorem smooth_finsum_cond {ΞΉ : Type u_1} {π•œ : Type u_2} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_3} [TopologicalSpace H] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_5} [AddCommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : ΞΉ β†’ M β†’ G} {p : ΞΉ β†’ Prop} (hc : βˆ€ (i : ΞΉ), p i β†’ ContMDiff I' I n (f i)) (hf : LocallyFinite fun (i : ΞΉ) => Function.support (f i)) :
      ContMDiff I' I n fun (x : M) => βˆ‘αΆ  (i : ΞΉ) (_ : p i), f i x

      Alias of contMDiff_finsum_cond.

      instance instContMDiffAddSelf {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {n : WithTop β„•βˆž} :
      theorem ContMDiffWithinAt.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} {s : Set M} {x : M} (c : G) (hf : ContMDiffWithinAt I' I n f s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => f x / c) s x
      theorem ContMDiffWithinAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : M β†’ G} {s : Set M} {x : M} (c : G) (hf : ContMDiffWithinAt I' I n f s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => f x - c) s x
      theorem ContMDiffAt.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} {x : M} (c : G) (hf : ContMDiffAt I' I n f x) :
      ContMDiffAt I' I n (fun (x : M) => f x / c) x
      theorem ContMDiffAt.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : M β†’ G} {x : M} (c : G) (hf : ContMDiffAt I' I n f x) :
      ContMDiffAt I' I n (fun (x : M) => f x - c) x
      theorem ContMDiffOn.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} {s : Set M} (c : G) (hf : ContMDiffOn I' I n f s) :
      ContMDiffOn I' I n (fun (x : M) => f x / c) s
      theorem ContMDiffOn.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : M β†’ G} {s : Set M} (c : G) (hf : ContMDiffOn I' I n f s) :
      ContMDiffOn I' I n (fun (x : M) => f x - c) s
      theorem ContMDiff.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} (c : G) (hf : ContMDiff I' I n f) :
      ContMDiff I' I n fun (x : M) => f x / c
      theorem ContMDiff.sub_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffAdd I n 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 : M β†’ G} (c : G) (hf : ContMDiff I' I n f) :
      ContMDiff I' I n fun (x : M) => f x - c
      @[deprecated ContMDiffWithinAt.div_const (since := "2024-11-21")]
      theorem SmoothWithinAt.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} {s : Set M} {x : M} (c : G) (hf : ContMDiffWithinAt I' I n f s x) :
      ContMDiffWithinAt I' I n (fun (x : M) => f x / c) s x

      Alias of ContMDiffWithinAt.div_const.

      @[deprecated ContMDiffAt.div_const (since := "2024-11-21")]
      theorem SmoothAt.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} {x : M} (c : G) (hf : ContMDiffAt I' I n f x) :
      ContMDiffAt I' I n (fun (x : M) => f x / c) x

      Alias of ContMDiffAt.div_const.

      @[deprecated ContMDiffOn.div_const (since := "2024-11-21")]
      theorem SmoothOn.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} {s : Set M} (c : G) (hf : ContMDiffOn I' I n f s) :
      ContMDiffOn I' I n (fun (x : M) => f x / c) s

      Alias of ContMDiffOn.div_const.

      @[deprecated ContMDiff.div_const (since := "2024-11-21")]
      theorem Smooth.div_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {n : WithTop β„•βˆž} {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace π•œ E] {I : ModelWithCorners π•œ E H} {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I n 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 : M β†’ G} (c : G) (hf : ContMDiff I' I n f) :
      ContMDiff I' I n fun (x : M) => f x / c

      Alias of ContMDiff.div_const.