torusMap_sub_center

Mathlib.MeasureTheory.Integral.TorusIntegral

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

English

Subtracting the center from torusMap gives the same as torusMap with zero center.

Русский

Отняв центр, получаем torusMap с нулевым центром.

LaTeX

$$$\\torusMap(c,R,\\theta) - c = \\torusMap(0,R,\\theta)$$$

Lean4

theorem torusMap_sub_center (c : ℂⁿ) (R : ℝⁿ) (θ : ℝⁿ) : torusMap c R θ - c = torusMap 0 R θ := by ext1 i;
  simp [torusMap]

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

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

Разделы

Аффилиация

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