Commit 2026-10-13 18:29 2ca3a6c4

View on Github →

refactor: review of SetSemiring (#37603)

  • Rename Set.up and SetSemiring.down to SetSemiring.ofSet and SetSemiring.toSet respectively. Unprotect both and make them equivalences, following FreeMonoid.
  • Derive CompleteAtomicBooleanAlgebra for SetSemiring immediately.
  • Add imageHom_id and imageHom_comp. The three existing lemmas about imageHom are coalesced into imageHom_apply. Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568.

Estimated changes

deleted theorem Set.up_empty
deleted theorem Set.up_image
deleted theorem Set.up_mul
deleted theorem Set.up_one
deleted theorem Set.up_union
modified theorem SetSemiring.add_def
deleted theorem SetSemiring.down_add
deleted theorem SetSemiring.down_imageHom
deleted theorem SetSemiring.down_mul
deleted theorem SetSemiring.down_one
deleted theorem SetSemiring.down_zero
deleted theorem SetSemiring.imageHom_def
modified theorem SetSemiring.mul_def
added theorem SetSemiring.ofSet_mul
added theorem SetSemiring.ofSet_one
modified theorem SetSemiring.one_def
added theorem SetSemiring.symm_ofSet
added theorem SetSemiring.symm_toSet
added theorem SetSemiring.toSet_add
added theorem SetSemiring.toSet_mul
added theorem SetSemiring.toSet_one
added theorem SetSemiring.toSet_zero
deleted theorem SetSemiring.up_le_up
deleted theorem SetSemiring.up_lt_up
modified theorem SetSemiring.zero_def
modified def SetSemiring