Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-22 19:28 841ac1a3

View on Github →

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

Estimated changes