Skip to content

Commit e73893a

Browse files
author
mjasper
committed
revert change that's no longer needed
1 parent be15dc5 commit e73893a

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,6 @@ lemma norm_jacobiTheta₂_term_fderiv_ge (n : ℤ) (z τ : ℂ) :
191191
simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
192192
Int.cast_abs, ← norm_intCast, norm_pow]
193193

194-
set_option backward.isDefEq.respectTransparency false in
195194
lemma summable_jacobiTheta₂_term_fderiv_iff (z τ : ℂ) :
196195
Summable (jacobiTheta₂_term_fderiv · z τ) ↔ 0 < im τ := by
197196
constructor

0 commit comments

Comments
 (0)