Commit 2023-06-10 02:10 9dd22b87

View on Github →

chore: use ofReal instead of of_real in lemma names (#4934)

Estimated changes

Modified Mathlib/Analysis/Complex/RealDeriv.lean

added theorem HasDerivAt.comp_ofReal

deleted theorem HasDerivAt.comp_of_real

added theorem HasDerivAt.ofReal_comp

deleted theorem HasDerivAt.of_real_comp

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

added theorem Complex.arg_ofReal_of_neg

added theorem Complex.arg_ofReal_of_nonneg

deleted theorem Complex.arg_of_real_of_neg

deleted theorem Complex.arg_of_real_of_nonneg

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

added theorem Complex.log_mul_ofReal

deleted theorem Complex.log_mul_of_real

added theorem Complex.log_ofReal_mul

added theorem Complex.log_ofReal_re

deleted theorem Complex.log_of_real_mul

deleted theorem Complex.log_of_real_re

added theorem Complex.ofReal_log

deleted theorem Complex.of_real_log

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

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

added theorem Complex.mul_cpow_ofReal_nonneg

deleted theorem Complex.mul_cpow_of_real_nonneg

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

added theorem Complex.continuousAt_ofReal_cpow

added theorem Complex.continuousAt_ofReal_cpow_const

deleted theorem Complex.continuousAt_of_real_cpow

deleted theorem Complex.continuousAt_of_real_cpow_const

added theorem Complex.continuous_ofReal_cpow_const

deleted theorem Complex.continuous_of_real_cpow_const

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

added theorem hasDerivAt_ofReal_cpow

deleted theorem hasDerivAt_of_real_cpow

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

added theorem Complex.ofReal_cpow

added theorem Complex.ofReal_cpow_of_nonpos

deleted theorem Complex.of_real_cpow

deleted theorem Complex.of_real_cpow_of_nonpos

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean

added theorem Polynomial.Chebyshev.complex_ofReal_eval_T

added theorem Polynomial.Chebyshev.complex_ofReal_eval_U

deleted theorem Polynomial.Chebyshev.complex_of_real_eval_T

deleted theorem Polynomial.Chebyshev.complex_of_real_eval_U

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean

Modified Mathlib/Data/Complex/Exponential.lean

added theorem Complex.sinh_ofReal_im

added theorem Complex.sinh_ofReal_re

deleted theorem Complex.sinh_of_real_im

deleted theorem Complex.sinh_of_real_re

added theorem Complex.tan_ofReal_im

added theorem Complex.tan_ofReal_re

deleted theorem Complex.tan_of_real_im

deleted theorem Complex.tan_of_real_re

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

added theorem Complex.measurable_ofReal

deleted theorem Complex.measurable_of_real

Modified Mathlib/NumberTheory/LSeries.lean