@[reducible, inline]

noncomputable abbrev η : ℂ → ℂ

Equations

• η = ModularForm.eta

theorem eta_logDeriv_eql (z : UpperHalfPlane) : logDeriv (η ∘ fun (z : ℂ) => -1 / z) ↑z = logDeriv (csqrt * η) ↑z

theorem eta_logderivs : Set.EqOn (logDeriv (η ∘ fun (z : ℂ) => -1 / z)) (logDeriv (csqrt * η)) {z : ℂ | 0 < z.im}

theorem eta_logderivs_const : ∃ (z : ℂ), z ≠ 0 ∧ Set.EqOn (η ∘ fun (z : ℂ) => -1 / z) (z • (csqrt * η)) {z : ℂ | 0 < z.im}

theorem eta_equality : Set.EqOn (η ∘ fun (z : ℂ) => -1 / z) ((csqrt Complex.I)⁻¹ • (csqrt * η)) {z : ℂ | 0 < z.im}