ordinaryHypergeometricSeries_symm

English

The ordinary hypergeometric series is symmetric in a and b: exchanging a and b leaves the series unchanged.

Русский

Обыкновенный гипергеометрический ряд симметричен относительно параметров a и b: при обмене a и b ряд не меняется.

LaTeX

$$$\\ordinaryHypergeometricSeries(a,b,c) = \\ordinaryHypergeometricSeries(b,a,c)$$$

Lean4

theorem ordinaryHypergeometricSeries_symm :
    ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c :=
  by
  unfold ordinaryHypergeometricSeries ordinaryHypergeometricCoefficient
  simp [mul_assoc, mul_left_comm]

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