mathlib3

841ac1a3 - refactor(algebra/lie): replace local instance with type synonym (#16154)

refactor(algebra/lie): replace local instance with type synonym (#16154) A Lie ring can be viewed as a `non_unital_non_assoc_semiring` by using its bracket operator as the multiplication. Defining this as an instance causes diamonds because all rings are also Lie rings, so there are two incompatible multiplications on the same type. Instead of the previous approach, of making this a `def` and only locally enabling the instance being careful not to cause diamonds, we use a type synonym that is guaranteed to have only one multiplication operator. Someone who knows more about Lie theory should definitely check that the changes make mathematical sense. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60lie_ring.2Eto_non_unital_non_assoc_semiring.60