Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-16 13:42 909b6732

View on Github →

split(data/set/semiring): Split off data.set.pointwise (#14145) Move set_semiring to a new file data.set.semiring. Crediting Floris for #3240

Estimated changes

Modified src/algebra/algebra/operations.lean

Modified src/data/set/pointwise.lean

deleted theorem set.down_ssubset_down

deleted theorem set.down_subset_down

deleted def set.image_hom

deleted theorem set.up_le_up

deleted theorem set.up_lt_up

Created src/data/set/semiring.lean

added theorem set_semiring.down_ssubset_down

added theorem set_semiring.down_subset_down

added def set_semiring.image_hom

added theorem set_semiring.up_le_up

added theorem set_semiring.up_lt_up