integral_const_mul

Mathlib.MeasureTheory.Integral.CircleIntegral

URI: https://scilib.ai/kg/mathlib#circleIntegral.integral_const_mul

← MathLib Explorer

English

If the circle has radius zero and f is any function, the circle integral is zero.

Русский

Если радиус окружности равен нулю, то круговой интеграл любой функции равен нулю.

LaTeX

$$$\\oint z in C(c,0), f(z) = 0$$$

Lean4

@[simp]
theorem integral_const_mul (a : ℂ) (f : ℂ → ℂ) (c : ℂ) (R : ℝ) : (∮ z in C(c, R), a * f z) = a * ∮ z in C(c, R), f z :=
  integral_smul a f c R

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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