Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.inv_one_sub_sq_eq_mul_inv_one_sub_one_add

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:152 to 165

Source documentation

(1 - z²)⁻¹ = (1 - z)⁻¹ · (1 + z)⁻¹ for ‖z‖ < 1.

Exact Lean statement

lemma inv_one_sub_sq_eq_mul_inv_one_sub_one_add (z : ℂ) (hz : ‖z‖ < 1) :
    (1 - z ^ 2)⁻¹ = (1 - z)⁻¹ * (1 + z)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma inv_one_sub_sq_eq_mul_inv_one_sub_one_add (z : ℂ) (hz : ‖z‖ < 1) :    (1 - z ^ 2)⁻¹ = (1 - z)⁻¹ * (1 + z)⁻¹ := by  have hz0 : 1 - z ≠ 0 := by    intro h    have : z = 1 := (sub_eq_zero.mp h).symm    simp [this, norm_one] at hz  have hz1 : 1 + z ≠ 0 := by    intro h    have : z = -1 := by exact Eq.symm (neg_eq_of_add_eq_zero_right h)    simp [this, norm_neg, norm_one] at hz  calc    (1 - z ^ 2)⁻¹ = ((1 - z) * (1 + z))⁻¹ := by ring    _ = (1 + z)⁻¹ * (1 - z)⁻¹ := by simp [mul_inv_rev]    _ = (1 - z)⁻¹ * (1 + z)⁻¹ := by ring