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.

src/algebra/group_with_zero/basic.lean

@@ -90,6 +90,12 @@ lemma mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) :
   a * b = 0 :=
 if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
 
+/-- To match `one_mul_eq_id`. -/
+lemma zero_mul_eq_const : ((*) (0 : M₀)) = function.const _ 0 := funext zero_mul
+
+/-- To match `mul_one_eq_id`. -/
+lemma mul_zero_eq_const : (* (0 : M₀)) = function.const _ 0 := funext mul_zero
+
 end mul_zero_class
 
 /-- Pushforward a `no_zero_divisors` instance along an injective function. -/