Commit 2026-03-06 16:20 4dafe2dc

View on Github →

chore(Probability): fix typo in namespace (#36253)

Estimated changes

Modified Mathlib/Probability/Distributions/Cauchy.lean

deleted theorem Probability.cauchyMeasure_of_scale_ne_zero

deleted theorem Probability.cauchyMeasure_zero_scale

deleted theorem Probability.cauchyPDFReal_def'

deleted theorem Probability.cauchyPDFReal_def

deleted theorem Probability.cauchyPDFReal_scale_zero

deleted theorem Probability.cauchyPDF_def

deleted theorem Probability.cauchyPDF_pos

deleted theorem Probability.cauchyPDF_scale_zero

deleted theorem Probability.integrable_cauchyPDFReal

deleted theorem Probability.integral_cauchyPDFReal

deleted theorem Probability.lintegral_cauchyPDF_eq_one

deleted theorem Probability.measurable_cauchyPDF

deleted theorem Probability.measurable_cauchyPDFReal

deleted theorem Probability.stronglyMeasurable_cauchyPDF

deleted theorem Probability.stronglyMeasurable_cauchyPDFReal

added theorem ProbabilityTheory.cauchyMeasure_of_scale_ne_zero

added theorem ProbabilityTheory.cauchyMeasure_zero_scale

added theorem ProbabilityTheory.cauchyPDFReal_def'

added theorem ProbabilityTheory.cauchyPDFReal_def

added theorem ProbabilityTheory.cauchyPDFReal_scale_zero

added theorem ProbabilityTheory.cauchyPDF_def

added theorem ProbabilityTheory.cauchyPDF_pos

added theorem ProbabilityTheory.cauchyPDF_scale_zero

added theorem ProbabilityTheory.integrable_cauchyPDFReal

added theorem ProbabilityTheory.integral_cauchyPDFReal_eq_one

added theorem ProbabilityTheory.lintegral_cauchyPDF_eq_one

added theorem ProbabilityTheory.measurable_cauchyPDF

added theorem ProbabilityTheory.measurable_cauchyPDFReal

added theorem ProbabilityTheory.stronglyMeasurable_cauchyPDF

added theorem ProbabilityTheory.stronglyMeasurable_cauchyPDFReal