Commit 2022-08-22 19:28 841ac1a3

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