Commit 2021-06-07 15:40 ef7aa94e

View on Github →

feat(algebra/ring/basic): define non-unital, non-associative rings (#6786) This introduces the following typeclasses beneath semiring:

  • non_unital_non_assoc_semiring
  • non_unital_semiring
  • non_assoc_semiring The goal is to use these to support a non-unital, non-associative algebras. The typeclass requirements of subring, subsemiring, and ring_hom are relaxed from semiring to non_assoc_semiring. Instances of these new typeclasses are added for:
  • alias types:
    • opposite
    • ulift
  • convolutive types:
    • (add_)monoid_algebra
    • direct_sum
    • set_semiring
    • hahn_series
  • elementwise types:
    • locally_constant
    • pi
    • prod
    • finsupp

Estimated changes

modified theorem add_monoid_hom.coe_mul_left
modified theorem boole_mul
modified theorem mul_boole
modified theorem ring_hom.comp_assoc
modified def ring_hom.id
modified theorem ring_hom.injective_iff
modified theorem ring_hom.is_unit_map
modified def ring_hom.mk'
modified structure ring_hom
modified theorem nat.cast_comm
modified theorem nat.cast_commute
modified theorem nat.cast_mul
modified def nat.cast_ring_hom
modified theorem nat.coe_cast_ring_hom