Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 17:30 2891e1be

View on Github →

feat(algebra/category/BoolRing): The category of Boolean rings (#12905) Define BoolRing, the category of Boolean rings.

Estimated changes

added theorem BoolRing.coe_of
added def BoolRing.iso.mk
added def BoolRing.of
added def BoolRing
modified theorem punit.div_eq
modified theorem punit.inv_eq
added def as_boolalg
modified def boolean_ring.has_sup
added def of_boolalg
added theorem of_boolalg_bot
added theorem of_boolalg_inf
added theorem of_boolalg_inj
added theorem of_boolalg_sup
added theorem of_boolalg_symm_eq
added theorem of_boolalg_to_boolalg
added theorem of_boolalg_top
added theorem ring_hom.as_boolalg_id
added def to_boolalg
added theorem to_boolalg_add_add_mul
added theorem to_boolalg_inj
added theorem to_boolalg_mul
added theorem to_boolalg_of_boolalg
added theorem to_boolalg_one
added theorem to_boolalg_symm_eq
added theorem to_boolalg_zero