Commit 2023-08-31 08:18 85c04e73

View on Github ā†’

refactor(Algebra/Star/*): Allow for star operation on non-associative algebras (#6562) Typically a * operation on a mathematical structure R equipped with a multiplication is an involutive anti-automorphism i.e.

āˆ€ r s : R, star (r * s) = star s * star r

Currently mathlib defines a class StarSemigroup to be a semigroup satisfying this property. However, the requirement for the multiplication to be associative is unnecessarily restrictive. There are important classes of star-algebra which are not associative (e.g. JB*-algebras). This PR removes the requirement for a StarSemigroup to be a semigroup, merely requiring it to have a multiplication. I've changed the name from StarSemigroup to StarMul since it's no longer a semigroup. Zulip discussion Previously opened as a mathlib PR https://github.com/leanprover-community/mathlib/pull/17949

Estimated changes

modified theorem IsUnit.star
modified theorem isUnit_star
modified def starMulAut
modified def starMulEquiv
added def starMulOfComm
modified def starRingEquiv
deleted def starSemigroupOfComm
modified theorem star_div
modified theorem star_inv
modified theorem star_invOf
modified theorem star_mul'
modified theorem star_natCast
modified theorem star_ofNat
modified theorem star_one
modified theorem star_pow
modified theorem star_zpow
modified theorem star_prod
modified structure IsCHSHTuple
modified theorem Units.embed_product_star
modified theorem IsSelfAdjoint.mul_star_self
modified theorem IsSelfAdjoint.star_mul_self
modified def unitary