mathlib

463be884 - feat(algebra/group_with_zero): add zero_mul_eq_const and mul_zero_eq_const (#11021)

feat(algebra/group_with_zero): add zero_mul_eq_const and mul_zero_eq_const (#11021) These are to match the corresponding lemmas about unapplied application of multiplication by 1. Like those lemmas, these are not marked simp.