Theorem ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity

Modification history

2025-06-05 23:26
Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
chore: update batteries dependency (including fixes for batteries#1220) (#25478)
Modified ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximityView on Github →
2025-06-02 06:15
Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
feat: introduce the Characteristic Function of Value Distribution Theory (#25014) …
Added ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximityView on Github →