Mathlib Changelog
v4
Changelog
About
Github
Theorem
ValueDistribution.proximity_coe_eq_proximity_sub_const_zero
Modification history
2025-05-15 08:18
Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean
feat: introduce the Proximity Function of Value Distribution Theory (#24876) …
Added
ValueDistribution.proximity_coe_eq_proximity_sub_const_zero
View on Github →