α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ ↑normalize 0 = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ x = 0 → ↑normalize x = 0
rintro rfl
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ ↑normalize 0 = 0
exact normalize_zero