Commit 2025-01-02 18:44 f8c0388c

View on Github →

chore(Analysis/SpecialFunctions/Pow/Complex): fix lemma name (#20406)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

deleted theorem Complex.cpow_natCast_add_one_ne_zero

added theorem Complex.natCast_add_one_cpow_ne_zero

Modified Mathlib/NumberTheory/LSeries/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Injectivity.lean