Commit 2023-01-20 18:06 2847b3b5

View on Github →

feat: port Data.Finite.Basic (#1722)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finite/Basic.lean

added theorem Finite.prod_left

added theorem Finite.prod_right

added theorem Finite.sum_left

added theorem Finite.sum_right