Commit 2024-11-26 05:23 c912bed7

View on Github →

chore(NumberTheory/LSeries/PrimesInAP): fix name (Lfunction -> LFunction) (#19474)

Estimated changes

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

added theorem ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux_real

deleted theorem ArithmeticFunction.vonMangoldt.LfunctionResidueClassAux_real

added theorem ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux'

added theorem ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux

deleted theorem ArithmeticFunction.vonMangoldt.continuousOn_LfunctionResidueClassAux'

deleted theorem ArithmeticFunction.vonMangoldt.continuousOn_LfunctionResidueClassAux

added theorem ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux

deleted theorem ArithmeticFunction.vonMangoldt.eqOn_LfunctionResidueClassAux