mathlib3

836184a8 - feat(tactic/protect_proj): protect_proj attribute for structures (#2855)

feat(tactic/protect_proj): protect_proj attribute for structures (#2855) This attribute protect the projections of a structure that is being defined. There were some errors in Euclidean domain caused by `rw` using `euclidean_domain.mul_assoc` instead of `mul_assoc` because the `euclidean_domain` namespace was open. This fixes this problem, and makes the `group` and `ring` etc. namespaces more usable. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>