Commit 2023-05-12 05:31 0ace8032

View on Github →

feat: Port Algebra.Ring.BooleanRing (#2104)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/BooleanRing.lean

added def AsBoolAlg

added def AsBoolRing

added def BooleanAlgebra.toBooleanRing

added def BooleanRing.inf

added theorem BooleanRing.inf_assoc

added theorem BooleanRing.inf_comm

added theorem BooleanRing.inf_sup_self

added theorem BooleanRing.le_sup_inf

added theorem BooleanRing.le_sup_inf_aux

added def BooleanRing.sup

added theorem BooleanRing.sup_assoc

added theorem BooleanRing.sup_comm

added theorem BooleanRing.sup_inf_self

added def BooleanRing.toBooleanAlgebra

added theorem BoundedLatticeHom.asBoolRing_comp

added theorem BoundedLatticeHom.asBoolRing_id

added def GeneralizedBooleanAlgebra.toNonUnitalCommRing

added def OrderIso.asBoolAlgAsBoolRing

added def RingEquiv.asBoolRingAsBoolAlg

added theorem RingHom.asBoolAlg_comp

added theorem RingHom.asBoolAlg_id

added theorem add_eq_zero'

added theorem add_self

added theorem mul_add_mul

added theorem mul_one_add_self

added theorem mul_self

added theorem neg_eq

added def ofBoolAlg

added theorem ofBoolAlg_bot

added theorem ofBoolAlg_compl

added theorem ofBoolAlg_inf

added theorem ofBoolAlg_inj

added theorem ofBoolAlg_mul_ofBoolAlg_eq_left_iff

added theorem ofBoolAlg_sdiff

added theorem ofBoolAlg_sup

added theorem ofBoolAlg_symmDiff

added theorem ofBoolAlg_symm_eq

added theorem ofBoolAlg_toBoolAlg

added theorem ofBoolAlg_top

added def ofBoolRing

added theorem ofBoolRing_add

added theorem ofBoolRing_inj

added theorem ofBoolRing_le_ofBoolRing_iff

added theorem ofBoolRing_mul

added theorem ofBoolRing_neg

added theorem ofBoolRing_one

added theorem ofBoolRing_sub

added theorem ofBoolRing_symm_eq

added theorem ofBoolRing_toBoolRing

added theorem ofBoolRing_zero

added theorem sub_eq_add

added def toBoolAlg

added theorem toBoolAlg_add

added theorem toBoolAlg_add_add_mul

added theorem toBoolAlg_inj

added theorem toBoolAlg_mul

added theorem toBoolAlg_ofBoolAlg

added theorem toBoolAlg_one

added theorem toBoolAlg_symm_eq

added theorem toBoolAlg_zero

added def toBoolRing

added theorem toBoolRing_bot

added theorem toBoolRing_inf

added theorem toBoolRing_inj

added theorem toBoolRing_ofBoolRing

added theorem toBoolRing_symmDiff

added theorem toBoolRing_symm_eq

added theorem toBoolRing_top