Commit 2022-04-10 01:48 3fe5c932

View on Github →

feat(algebra/ring/boolean_ring): Turning a Boolean algebra into a Boolean ring (#6476) Define as_boolring, a type synonym to turn a Boolean algebra into a Boolean ring and show that as_boolring and as_boolalg are "inverse" to each other.

Estimated changes

Modified src/algebra/category/BoolRing.lean

Modified src/algebra/ring/boolean_ring.lean

added def as_boolring

added def boolean_algebra.to_boolean_ring

added theorem bounded_lattice_hom.as_boolring_comp

added theorem bounded_lattice_hom.as_boolring_id

added def generalized_boolean_algebra.to_non_unital_ring

added theorem of_boolalg_compl

added theorem of_boolalg_mul_of_boolalg_eq_left_iff

added theorem of_boolalg_sdiff

added theorem of_boolalg_symm_diff

added def of_boolring

added theorem of_boolring_add

added theorem of_boolring_inj

added theorem of_boolring_le_of_boolring_iff

added theorem of_boolring_mul

added theorem of_boolring_neg

added theorem of_boolring_one

added theorem of_boolring_sub

added theorem of_boolring_symm_eq

added theorem of_boolring_to_boolring

added theorem of_boolring_zero

added def order_iso.as_boolalg_as_boolring

added def ring_equiv.as_boolring_as_boolalg

added theorem to_boolalg_add

modified theorem to_boolalg_add_add_mul

added def to_boolring

added theorem to_boolring_bot

added theorem to_boolring_inf

added theorem to_boolring_inj

added theorem to_boolring_of_boolring

added theorem to_boolring_symm_diff

added theorem to_boolring_symm_eq

added theorem to_boolring_top

Modified src/order/hom/lattice.lean

added theorem disjoint.map

added theorem is_compl.map

added theorem map_compl

added theorem map_sdiff

added theorem map_symm_diff