Commit 2023-01-13 15:16 1e38b243

View on Github →

feat: Port Data.Set.Semiring (#1535)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Semiring.lean

added theorem SetSemiring.down_ssubset_down

added theorem SetSemiring.down_subset_down

added def SetSemiring.imageHom

added theorem SetSemiring.up_le_up

added theorem SetSemiring.up_lt_up

added def SetSemiring