Gamma_conj — Mathlib

English

Γ(conj s) = conj(Γ(s)).

Русский

Γ(conj s) = conj(Γ(s)).

LaTeX

$$$$ \Gamma(\overline{s}) = \overline{\Gamma(s)}. $$$$

Lean4

theorem Gamma_conj (s : ℂ) : Gamma (conj s) = conj (Gamma s) :=
  by
  suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by simp [Gamma, this]
  intro n
  induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, RingHom.map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [RingHom.map_add, RingHom.map_one]

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