BooleanRing

📁 Source: Mathlib/Algebra/Ring/BooleanRing.lean

Statistics

Metric	Count
Definitions AsBoolAlg, AsBoolRing, toBooleanRing, BooleanRing, inf, sup, toBooleanAlgebra, toCommRing, toRing, asBoolRing, toNonUnitalCommRing, asBoolAlgAsBoolRing, asBoolRingAsBoolAlg, asBoolAlg, instAddBool_mathlib, instBooleanAlgebraAsBoolAlg, instBooleanRingAsBoolRing, instBooleanRingBool, instBooleanRingPUnit, instInhabitedAsBoolAlg, instInhabitedAsBoolRing, instMulBool_mathlib, instNegBool_mathlib, instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra, instOneBool_mathlib, instSubBool_mathlib, instZeroBool_mathlib, ofBoolAlg, ofBoolRing, toBoolAlg, toBoolRing	31
Theorems add_eq_zero', add_self, inf_assoc, inf_comm, inf_sup_self, instIdempotentOpHMul, isIdempotentElem, le_sup_inf, le_sup_inf_aux, mul_add_mul, mul_one_add_self, mul_self, neg_eq, sub_eq_add, sup_assoc, sup_comm, sup_inf_self, asBoolRing_apply, asBoolRing_comp, asBoolRing_id, asBoolAlgAsBoolRing_apply, asBoolAlgAsBoolRing_symm_apply, asBoolRingAsBoolAlg_apply, asBoolRingAsBoolAlg_symm_apply, asBoolAlg_comp, asBoolAlg_id, asBoolAlg_toFun, ofBoolAlg_bot, ofBoolAlg_compl, ofBoolAlg_inf, ofBoolAlg_inj, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, ofBoolAlg_sdiff, ofBoolAlg_sup, ofBoolAlg_symmDiff, ofBoolAlg_symm_eq, ofBoolAlg_toBoolAlg, ofBoolAlg_top, ofBoolRing_add, ofBoolRing_inj, ofBoolRing_le_ofBoolRing_iff, ofBoolRing_mul, ofBoolRing_neg, ofBoolRing_one, ofBoolRing_sub, ofBoolRing_symm_eq, ofBoolRing_toBoolRing, ofBoolRing_zero, toBoolAlg_add, toBoolAlg_add_add_mul, toBoolAlg_inj, toBoolAlg_mul, toBoolAlg_ofBoolAlg, toBoolAlg_one, toBoolAlg_symm_eq, toBoolAlg_zero, toBoolRing_bot, toBoolRing_inf, toBoolRing_inj, toBoolRing_ofBoolRing, toBoolRing_symmDiff, toBoolRing_symm_eq, toBoolRing_top	63
Total	94

BooleanAlgebra

Definitions

Name	Category	Theorems
toBooleanRing 📖	CompOp	—

BooleanRing

Definitions

Name	Category	Theorems
inf 📖	CompOp	5 math math: sup_inf_self, inf_sup_self, le_sup_inf, inf_comm, inf_assoc
sup 📖	CompOp	5 math math: sup_inf_self, inf_sup_self, le_sup_inf, sup_comm, sup_assoc
toBooleanAlgebra 📖	CompOp	—
toCommRing 📖	CompOp	28 math math: BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, RingEquiv.asBoolRingAsBoolAlg_apply, BoolRing.Iso.mk_hom_hom', BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, BoolRing.Iso.mk_inv_hom', ofBoolAlg_inf, BoolAlg.hasForgetToBoolRing_forget₂_map, RingEquiv.asBoolRingAsBoolAlg_symm_apply, ofBoolAlg_bot, boolRingCatEquivBoolAlg_functor, toBoolAlg_zero, toBoolAlg_add, ofBoolAlg_sup, toBoolAlg_add_add_mul, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, ofBoolAlg_symmDiff, RingHom.asBoolAlg_id, RingHom.asBoolAlg_comp, ofBoolAlg_sdiff, boolRingCatEquivBoolAlg_inverse, BoundedLatticeHom.asBoolRing_apply, BoolRing.hasForgetToBoolAlg_forget₂_map, BoundedLatticeHom.asBoolRing_id, BoundedLatticeHom.asBoolRing_comp, le_sup_inf_aux, ofBoolAlg_compl, toBoolAlg_mul, RingHom.asBoolAlg_toFun
toRing 📖	CompOp	17 math math: ofBoolRing_one, ofBoolRing_sub, mul_self, neg_eq, instIdempotentOpHMul, add_self, sub_eq_add, ofBoolAlg_sdiff, add_eq_zero', ofBoolAlg_top, ofBoolRing_neg, isIdempotentElem, mul_add_mul, mul_one_add_self, toBoolRing_top, toBoolAlg_one, ofBoolAlg_compl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_zero' 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	add_eq_zero_iff_eq_neg neg_eq
add_self 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_self add_mul Distrib.rightDistribClass mul_add Distrib.leftDistribClass right_eq_add AddRightCancelSemigroup.toIsRightCancelAdd
inf_assoc 📖	mathematical	—	inf	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
inf_comm 📖	mathematical	—	inf	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
inf_sup_self 📖	mathematical	—	inf sup	—	mul_add Distrib.leftDistribClass mul_self mul_assoc add_assoc add_self add_zero
instIdempotentOpHMul 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toRing	—	mul_self
isIdempotentElem 📖	mathematical	—	IsIdempotentElem NonUnitalNonAssocSemiring.toMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring toRing	—	—
le_sup_inf 📖	mathematical	—	sup inf	—	le_sup_inf_aux add_self mul_self zero_add
le_sup_inf_aux 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing Distrib.toAdd	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf mul_self add_self add_zero
mul_add_mul 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_self add_mul Distrib.rightDistribClass mul_add Distrib.leftDistribClass Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero left_eq_add AddLeftCancelSemigroup.toIsLeftCancelAdd
mul_one_add_self 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toRing Distrib.toAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_add Distrib.leftDistribClass mul_one mul_self add_self
mul_self 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toRing	—	IsIdempotentElem.eq isIdempotentElem
neg_eq 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup toRing	—	add_zero neg_add_cancel add_assoc add_self zero_add
sub_eq_add 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_eq_add_neg AddLeftCancelSemigroup.toIsLeftCancelAdd neg_eq
sup_assoc 📖	mathematical	—	sup	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt
sup_comm 📖	mathematical	—	sup	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt
sup_inf_self 📖	mathematical	—	sup inf	—	mul_assoc mul_self add_assoc add_self add_zero

BoundedLatticeHom

Definitions

Name	Category	Theorems
asBoolRing 📖	CompOp	4 math math: BoolAlg.hasForgetToBoolRing_forget₂_map, asBoolRing_apply, asBoolRing_id, asBoolRing_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asBoolRing_apply 📖	mathematical	—	DFunLike.coe RingHom AsBoolRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing instBooleanRingAsBoolRing RingHom.instFunLike asBoolRing Equiv EquivLike.toFunLike Equiv.instEquivLike toBoolRing BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toBoundedOrder instFunLike ofBoolRing	—	—
asBoolRing_comp 📖	mathematical	—	asBoolRing comp GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toBoundedOrder RingHom.comp AsBoolRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing instBooleanRingAsBoolRing	—	—
asBoolRing_id 📖	mathematical	—	asBoolRing id GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toBoundedOrder RingHom.id AsBoolRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing instBooleanRingAsBoolRing	—	—

GeneralizedBooleanAlgebra

Definitions

Name	Category	Theorems
toNonUnitalCommRing 📖	CompOp	—

OrderIso

Definitions

Name	Category	Theorems
asBoolAlgAsBoolRing 📖	CompOp	2 math math: asBoolAlgAsBoolRing_apply, asBoolAlgAsBoolRing_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asBoolAlgAsBoolRing_apply 📖	mathematical	—	DFunLike.coe RelIso AsBoolAlg AsBoolRing Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg instBooleanRingAsBoolRing RelIso.instFunLike asBoolAlgAsBoolRing Equiv EquivLike.toFunLike Equiv.instEquivLike ofBoolRing ofBoolAlg	—	—
asBoolAlgAsBoolRing_symm_apply 📖	mathematical	—	DFunLike.coe RelIso AsBoolAlg AsBoolRing Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg instBooleanRingAsBoolRing RelIso.instFunLike RelIso.symm asBoolAlgAsBoolRing Equiv EquivLike.toFunLike Equiv.instEquivLike toBoolAlg toBoolRing	—	—

RingEquiv

Definitions

Name	Category	Theorems
asBoolRingAsBoolAlg 📖	CompOp	2 math math: asBoolRingAsBoolAlg_apply, asBoolRingAsBoolAlg_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asBoolRingAsBoolAlg_apply 📖	mathematical	—	DFunLike.coe RingEquiv AsBoolRing AsBoolAlg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra instBooleanAlgebraAsBoolAlg CommRing.toNonUnitalCommRing BooleanRing.toCommRing Distrib.toAdd EquivLike.toFunLike instEquivLike asBoolRingAsBoolAlg Equiv Equiv.instEquivLike ofBoolAlg ofBoolRing	—	—
asBoolRingAsBoolAlg_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv AsBoolRing AsBoolAlg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra instBooleanAlgebraAsBoolAlg Distrib.toAdd EquivLike.toFunLike instEquivLike symm asBoolRingAsBoolAlg Equiv Equiv.instEquivLike toBoolRing toBoolAlg	—	—

RingHom

Definitions

Name	Category	Theorems
asBoolAlg 📖	CompOp	4 math math: asBoolAlg_id, asBoolAlg_comp, BoolRing.hasForgetToBoolAlg_forget₂_map, asBoolAlg_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asBoolAlg_comp 📖	mathematical	—	asBoolAlg comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing BoundedLatticeHom.comp AsBoolAlg GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg BooleanAlgebra.toBoundedOrder	—	—
asBoolAlg_id 📖	mathematical	—	asBoolAlg id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing BoundedLatticeHom.id AsBoolAlg GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg BooleanAlgebra.toBoundedOrder	—	—
asBoolAlg_toFun 📖	mathematical	—	DFunLike.coe BoundedLatticeHom AsBoolAlg GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike asBoolAlg Equiv EquivLike.toFunLike Equiv.instEquivLike toBoolAlg RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing instFunLike ofBoolAlg	—	—

(root)

Definitions

Name	Category	Theorems
AsBoolAlg 📖	CompOp	28 math math: BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, RingEquiv.asBoolRingAsBoolAlg_apply, ofBoolAlg_inj, ofBoolAlg_inf, RingEquiv.asBoolRingAsBoolAlg_symm_apply, ofBoolAlg_bot, toBoolAlg_zero, toBoolAlg_add, ofBoolAlg_sup, toBoolAlg_add_add_mul, ofBoolAlg_symm_eq, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, toBoolAlg_symm_eq, ofBoolAlg_symmDiff, RingHom.asBoolAlg_id, RingHom.asBoolAlg_comp, ofBoolAlg_sdiff, BoolRing.hasForgetToBoolAlg_forget₂_map, ofBoolAlg_top, toBoolAlg_inj, OrderIso.asBoolAlgAsBoolRing_apply, ofBoolAlg_toBoolAlg, OrderIso.asBoolAlgAsBoolRing_symm_apply, toBoolAlg_one, toBoolAlg_ofBoolAlg, ofBoolAlg_compl, toBoolAlg_mul, RingHom.asBoolAlg_toFun
AsBoolRing 📖	CompOp	26 math math: ofBoolRing_one, ofBoolRing_sub, RingEquiv.asBoolRingAsBoolAlg_apply, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, toBoolRing_inf, toBoolRing_ofBoolRing, BoolAlg.hasForgetToBoolRing_forget₂_map, RingEquiv.asBoolRingAsBoolAlg_symm_apply, ofBoolRing_add, ofBoolRing_toBoolRing, ofBoolRing_le_ofBoolRing_iff, ofBoolRing_zero, BoundedLatticeHom.asBoolRing_apply, toBoolRing_symm_eq, ofBoolRing_inj, ofBoolRing_mul, BoundedLatticeHom.asBoolRing_id, ofBoolRing_neg, BoundedLatticeHom.asBoolRing_comp, OrderIso.asBoolAlgAsBoolRing_apply, toBoolRing_inj, toBoolRing_top, OrderIso.asBoolAlgAsBoolRing_symm_apply, toBoolRing_symmDiff, toBoolRing_bot, ofBoolRing_symm_eq
BooleanRing 📖	CompData	—
instAddBool_mathlib 📖	CompOp	—
instBooleanAlgebraAsBoolAlg 📖	CompOp	21 math math: RingEquiv.asBoolRingAsBoolAlg_apply, ofBoolAlg_inf, RingEquiv.asBoolRingAsBoolAlg_symm_apply, ofBoolAlg_bot, toBoolAlg_zero, toBoolAlg_add, ofBoolAlg_sup, toBoolAlg_add_add_mul, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, ofBoolAlg_symmDiff, RingHom.asBoolAlg_id, RingHom.asBoolAlg_comp, ofBoolAlg_sdiff, BoolRing.hasForgetToBoolAlg_forget₂_map, ofBoolAlg_top, OrderIso.asBoolAlgAsBoolRing_apply, OrderIso.asBoolAlgAsBoolRing_symm_apply, toBoolAlg_one, ofBoolAlg_compl, toBoolAlg_mul, RingHom.asBoolAlg_toFun
instBooleanRingAsBoolRing 📖	CompOp	10 math math: ofBoolRing_one, ofBoolRing_sub, BoolAlg.hasForgetToBoolRing_forget₂_map, BoundedLatticeHom.asBoolRing_apply, BoundedLatticeHom.asBoolRing_id, ofBoolRing_neg, BoundedLatticeHom.asBoolRing_comp, OrderIso.asBoolAlgAsBoolRing_apply, toBoolRing_top, OrderIso.asBoolAlgAsBoolRing_symm_apply
instBooleanRingBool 📖	CompOp	—
instBooleanRingPUnit 📖	CompOp	—
instInhabitedAsBoolAlg 📖	CompOp	—
instInhabitedAsBoolRing 📖	CompOp	—
instMulBool_mathlib 📖	CompOp	—
instNegBool_mathlib 📖	CompOp	—
instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra 📖	CompOp	9 math math: RingEquiv.asBoolRingAsBoolAlg_apply, toBoolRing_inf, RingEquiv.asBoolRingAsBoolAlg_symm_apply, ofBoolRing_add, ofBoolRing_le_ofBoolRing_iff, ofBoolRing_zero, ofBoolRing_mul, toBoolRing_symmDiff, toBoolRing_bot
instOneBool_mathlib 📖	CompOp	—
instSubBool_mathlib 📖	CompOp	—
instZeroBool_mathlib 📖	CompOp	—
ofBoolAlg 📖	CompOp	16 math math: RingEquiv.asBoolRingAsBoolAlg_apply, ofBoolAlg_inj, ofBoolAlg_inf, ofBoolAlg_bot, ofBoolAlg_sup, ofBoolAlg_symm_eq, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, toBoolAlg_symm_eq, ofBoolAlg_symmDiff, ofBoolAlg_sdiff, ofBoolAlg_top, OrderIso.asBoolAlgAsBoolRing_apply, ofBoolAlg_toBoolAlg, toBoolAlg_ofBoolAlg, ofBoolAlg_compl, RingHom.asBoolAlg_toFun
ofBoolRing 📖	CompOp	15 math math: ofBoolRing_one, ofBoolRing_sub, RingEquiv.asBoolRingAsBoolAlg_apply, toBoolRing_ofBoolRing, ofBoolRing_add, ofBoolRing_toBoolRing, ofBoolRing_le_ofBoolRing_iff, ofBoolRing_zero, BoundedLatticeHom.asBoolRing_apply, toBoolRing_symm_eq, ofBoolRing_inj, ofBoolRing_mul, ofBoolRing_neg, OrderIso.asBoolAlgAsBoolRing_apply, ofBoolRing_symm_eq
toBoolAlg 📖	CompOp	13 math math: RingEquiv.asBoolRingAsBoolAlg_symm_apply, toBoolAlg_zero, toBoolAlg_add, toBoolAlg_add_add_mul, ofBoolAlg_symm_eq, toBoolAlg_symm_eq, toBoolAlg_inj, ofBoolAlg_toBoolAlg, OrderIso.asBoolAlgAsBoolRing_symm_apply, toBoolAlg_one, toBoolAlg_ofBoolAlg, toBoolAlg_mul, RingHom.asBoolAlg_toFun
toBoolRing 📖	CompOp	12 math math: toBoolRing_inf, toBoolRing_ofBoolRing, RingEquiv.asBoolRingAsBoolAlg_symm_apply, ofBoolRing_toBoolRing, BoundedLatticeHom.asBoolRing_apply, toBoolRing_symm_eq, toBoolRing_inj, toBoolRing_top, OrderIso.asBoolAlgAsBoolRing_symm_apply, toBoolRing_symmDiff, toBoolRing_bot, ofBoolRing_symm_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofBoolAlg_bot 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg Bot.bot BooleanAlgebra.toBot instBooleanAlgebraAsBoolAlg MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing	—	—
ofBoolAlg_compl 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg Compl.compl BooleanAlgebra.toCompl instBooleanAlgebraAsBoolAlg Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne BooleanRing.toRing	—	—
ofBoolAlg_inf 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing	—	—
ofBoolAlg_inj 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg	—	—
ofBoolAlg_mul_ofBoolAlg_eq_left_iff 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg	—	inf_eq_left
ofBoolAlg_sdiff 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg BooleanAlgebra.toSDiff instBooleanAlgebraAsBoolAlg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing Distrib.toAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne BooleanRing.toRing	—	—
ofBoolAlg_sup 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing Distrib.toMul	—	—
ofBoolAlg_symmDiff 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg BooleanAlgebra.toSDiff Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing	—	symmDiff_eq_sup_sdiff_inf
ofBoolAlg_symm_eq 📖	mathematical	—	Equiv.symm AsBoolAlg ofBoolAlg toBoolAlg	—	—
ofBoolAlg_toBoolAlg 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg toBoolAlg	—	—
ofBoolAlg_top 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike ofBoolAlg Top.top BooleanAlgebra.toTop instBooleanAlgebraAsBoolAlg AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne BooleanRing.toRing	—	—
ofBoolRing_add 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toSDiff	—	—
ofBoolRing_inj 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing	—	—
ofBoolRing_le_ofBoolRing_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra	—	inf_eq_left
ofBoolRing_mul 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra	—	—
ofBoolRing_neg 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup BooleanRing.toRing instBooleanRingAsBoolRing	—	—
ofBoolRing_one 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne BooleanRing.toRing instBooleanRingAsBoolRing Top.top BooleanAlgebra.toTop	—	—
ofBoolRing_sub 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne BooleanRing.toRing instBooleanRingAsBoolRing symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toSDiff	—	—
ofBoolRing_symm_eq 📖	mathematical	—	Equiv.symm AsBoolRing ofBoolRing toBoolRing	—	—
ofBoolRing_toBoolRing 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing toBoolRing	—	—
ofBoolRing_zero 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike ofBoolRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra Bot.bot BooleanAlgebra.toBot	—	—
toBoolAlg_add 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg BooleanAlgebra.toSDiff	—	ofBoolAlg_symmDiff
toBoolAlg_add_add_mul 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing Distrib.toMul SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg	—	—
toBoolAlg_inj 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg	—	—
toBoolAlg_mul 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebraAsBoolAlg	—	—
toBoolAlg_ofBoolAlg 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg ofBoolAlg	—	—
toBoolAlg_one 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne BooleanRing.toRing Top.top BooleanAlgebra.toTop instBooleanAlgebraAsBoolAlg	—	—
toBoolAlg_symm_eq 📖	mathematical	—	Equiv.symm AsBoolAlg toBoolAlg ofBoolAlg	—	—
toBoolAlg_zero 📖	mathematical	—	DFunLike.coe Equiv AsBoolAlg EquivLike.toFunLike Equiv.instEquivLike toBoolAlg MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing Bot.bot BooleanAlgebra.toBot instBooleanAlgebraAsBoolAlg	—	—
toBoolRing_bot 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike toBoolRing Bot.bot BooleanAlgebra.toBot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra	—	—
toBoolRing_inf 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike toBoolRing SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra	—	—
toBoolRing_inj 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike toBoolRing	—	—
toBoolRing_ofBoolRing 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike toBoolRing ofBoolRing	—	—
toBoolRing_symmDiff 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike toBoolRing symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toSDiff Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing instNonUnitalCommRingAsBoolRingOfGeneralizedBooleanAlgebra BooleanAlgebra.toGeneralizedBooleanAlgebra	—	—
toBoolRing_symm_eq 📖	mathematical	—	Equiv.symm AsBoolRing toBoolRing ofBoolRing	—	—
toBoolRing_top 📖	mathematical	—	DFunLike.coe Equiv AsBoolRing EquivLike.toFunLike Equiv.instEquivLike toBoolRing Top.top BooleanAlgebra.toTop AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne BooleanRing.toRing instBooleanRingAsBoolRing	—	—

---

← Back to Index