Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-15 14:10 96315941

View on Github →

feat(algebra/star): star monoids, rings and algebras (#4886)

Estimated changes

added theorem star_smul
added def star
added theorem star_add
added def star_add_equiv
added theorem star_bit0
added theorem star_bit1
added theorem star_id_of_comm
added theorem star_injective
added theorem star_mul
added def star_mul_equiv
added theorem star_neg
added theorem star_one
added def star_ring_equiv
added theorem star_star
added theorem star_sub
added theorem star_sum
added theorem star_zero
added theorem matrix.map_map
added theorem matrix.star_apply