Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-02 02:44 cc9de07a

View on Github →

feat(algebra/star): replace star_monoid with star_semigroup (#12299) In preparation for allowing non-unital C^* algebras, replace star_monoid with star_semigroup.

Estimated changes

modified theorem is_unit.star
modified theorem is_unit_star
modified theorem star_div
modified theorem star_inv
modified theorem star_inv_of
deleted def star_monoid_of_comm
modified theorem star_mul'
modified def star_mul_aut
modified def star_mul_equiv
modified theorem star_mul_self_nonneg'
modified theorem star_mul_self_nonneg
modified theorem star_one
modified theorem star_pow
modified theorem star_prod
modified def star_ring_equiv
modified theorem star_zpow
modified structure is_CHSH_tuple
modified def unitary
modified theorem matrix.conj_transpose_smul