instContMDiffMulOfNatWithTopENatOfContinuousMul

Mathlib.Geometry.Manifold.Algebra.Monoid

URI: https://scilib.ai/kg/mathlib#instContMDiffMulOfNatWithTopENatOfContinuousMul

English

If ContMDiffMul I 2 G, then ContMDiffMul I 1 G by one-step downgrade.

Русский

Если ContMDiffMul I 2 G, тогда понижаем до ContMDiffMul I 1 G.

LaTeX

$$$$ \ContMDiffMul I 2 G \Rightarrow \ContMDiffMul I 1 G $$$$

Lean4

@[to_additive]
instance [ContinuousMul G] : ContMDiffMul I 0 G := by
  constructor
  rw [contMDiff_zero_iff]
  exact continuous_mul

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru