Theorems · Theorem · global analysis

ContMDiffSMul.contMDiff_smul

∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  {inst_4 : TopologicalSpace H'} {E' : Type u_5} {inst_5 : NormedAddCommGroup E'} {inst_6 : NormedSpace 𝕜 E'}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_6} {inst_7 : TopologicalSpace G}
  {inst_8 : ChartedSpace H G} {M : Type u_7} {inst_9 : TopologicalSpace M} {inst_10 : ChartedSpace H' M}
  {inst_11 : SMul G M} [self : ContMDiffSMul I I' n G M], ContMDiff (I.prod I') I' n fun p => p.1 • p.2

Defined in

Mathlib.Geometry.Manifold.Algebra.SMul

Cited by

5 results in Mathlib

Foundations

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

Assumes

ContMDiffSMul