Commit 2023-08-18 14:30 2e06bd9f

View on Github →

feat(Data/Sum): forall_sum_pi (#6658)

Estimated changes

Modified Mathlib/Data/Sum/Basic.lean

added theorem Sum.exists_sum_pi

added theorem Sum.forall_sum_pi