Theorems · Theorem · global analysis

ContMDiffMul.contMDiff_mul

∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Mul G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : ContMDiffMul I n G],
  ContMDiff (I.prod I) I n fun p => p.1 * p.2

Defined in

Mathlib.Geometry.Manifold.Algebra.Monoid

Cited by

2 results in Mathlib

Foundations

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

Assumes

ContMDiffMul