Mathlib v3 is deprecated. Go to Mathlib v4

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 def ulift.ring_equiv
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
modified theorem hahn_series.emb_domain_mul
modified theorem hahn_series.emb_domain_one
modified theorem hahn_series.mul_coeff
modified theorem hahn_series.mul_coeff_left'
modified theorem hahn_series.order_one
modified theorem hahn_series.support_one
modified theorem subsemiring.coe_pow
modified theorem subsemiring.list_prod_mem
modified theorem subsemiring.pow_mem
modified theorem subsemiring.smul_def
modified theorem subsemiring.sum_mem
modified structure subsemiring