mathlib

c7498d08 - feat(algebra/{group/with_one,order/monoid}): equivs for `with_zero` and `with_one` (#12275)

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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/with_zero.20.28multiplicative.20A.29.20.E2.89.83*.20multiplicative.20.28with_bot.20A.29/near/272980650)