Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-28 12:46 c7498d08

View on Github →

feat(algebra/{group/with_one,order/monoid}): equivs for with_zero and with_one (#12275) This provides:

  • add_equiv.with_zero_congr : α ≃+ β → with_zero α ≃+ with_zero β
  • mul_equiv.with_one_congr : α ≃* β → with_one α ≃* with_one β
  • with_zero.to_mul_bot : with_zero (multiplicative α) ≃* multiplicative (with_bot α) Zulip thread

Estimated changes

added theorem with_one.map_coe
modified theorem with_one.map_comp
added theorem with_one.map_map