Commit 2023-03-02 22:50 4bf8505b

View on Github →

feat: forward-port leanprover-community/mathlib#18449 (#2518) The diff being ported is https://github.com/leanprover-community/mathlib3port/commit/d034837787b3e04cf65ce061952078a6e75b66da#diff-968496f13ddf1f2e9b559f374e46c52125a2ada4f449bbce0989bc8ef4965e67. This also includes a fix from leanprover-community/mathlib#18539

Estimated changes

added theorem Set.up_empty
added theorem Set.up_image
added theorem Set.up_mul
added theorem Set.up_one
added theorem Set.up_union
added theorem SetSemiring.add_def
added theorem SetSemiring.down_add
added theorem SetSemiring.down_mul
added theorem SetSemiring.down_one
added theorem SetSemiring.down_zero
added theorem SetSemiring.mul_def
added theorem SetSemiring.one_def
added theorem SetSemiring.zero_def