BoolRing

📁 Source: Mathlib/Algebra/Category/BoolRing.lean

Statistics

Metric	Count
Definitions hasForgetToBoolRing, BoolRing, hom, hom', mk, booleanRing, carrier, hasForgetToBoolAlg, hasForgetToCommRing, instCategory, instCoeSortType, instConcreteCategoryRingHomCarrier, instInhabited, ofHom, boolRingCatEquivBoolAlg, instBooleanAlgebraCarrierToBddLatToBddDistLat, instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg	17
Theorems hasForgetToBoolRing_forget₂_map, hasForgetToBoolRing_forget₂_obj_carrier, ext, ext_iff, mk_hom_hom', mk_inv_hom', coe_of, hasForgetToBoolAlg_forget₂_map, hasForgetToBoolAlg_forget₂_obj_coe, hom_ext, hom_ext_iff, boolRingCatEquivBoolAlg_functor, boolRingCatEquivBoolAlg_inverse	13
Total	30

BoolAlg

Definitions

Name	Category	Theorems
hasForgetToBoolRing 📖	CompOp	3 math math: hasForgetToBoolRing_forget₂_obj_carrier, hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasForgetToBoolRing_forget₂_map 📖	mathematical	—	CategoryTheory.Functor.map BoolAlg instCategory BoolRing BoolRing.instCategory CategoryTheory.HasForget₂.forget₂ BoundedLatticeHom carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier RingHom BoolRing.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing BoolRing.booleanRing RingHom.instFunLike BoolRing.instConcreteCategoryRingHomCarrier hasForgetToBoolRing BoolRing.ofHom AsBoolRing instBooleanRingAsBoolRing BoundedLatticeHom.asBoolRing Hom.hom	—	—
hasForgetToBoolRing_forget₂_obj_carrier 📖	mathematical	—	BoolRing.carrier CategoryTheory.Functor.obj BoolAlg instCategory BoolRing BoolRing.instCategory CategoryTheory.HasForget₂.forget₂ BoundedLatticeHom carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing BoolRing.booleanRing RingHom.instFunLike BoolRing.instConcreteCategoryRingHomCarrier hasForgetToBoolRing AsBoolRing	—	—

BoolRing

Definitions

Name	Category	Theorems
booleanRing 📖	CompOp	8 math math: hasForgetToBoolAlg_forget₂_obj_coe, Iso.mk_hom_hom', BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, Iso.mk_inv_hom', BoolAlg.hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, boolRingCatEquivBoolAlg_inverse, hasForgetToBoolAlg_forget₂_map
carrier 📖	CompOp	9 math math: hasForgetToBoolAlg_forget₂_obj_coe, Iso.mk_hom_hom', BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, Iso.mk_inv_hom', BoolAlg.hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, coe_of, boolRingCatEquivBoolAlg_inverse, hasForgetToBoolAlg_forget₂_map
hasForgetToBoolAlg 📖	CompOp	3 math math: hasForgetToBoolAlg_forget₂_obj_coe, boolRingCatEquivBoolAlg_functor, hasForgetToBoolAlg_forget₂_map
hasForgetToCommRing 📖	CompOp	—
instCategory 📖	CompOp	8 math math: hasForgetToBoolAlg_forget₂_obj_coe, Iso.mk_hom_hom', BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, Iso.mk_inv_hom', BoolAlg.hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, boolRingCatEquivBoolAlg_inverse, hasForgetToBoolAlg_forget₂_map
instCoeSortType 📖	CompOp	—
instConcreteCategoryRingHomCarrier 📖	CompOp	6 math math: hasForgetToBoolAlg_forget₂_obj_coe, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, BoolAlg.hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, boolRingCatEquivBoolAlg_inverse, hasForgetToBoolAlg_forget₂_map
instInhabited 📖	CompOp	—
ofHom 📖	CompOp	1 math math: BoolAlg.hasForgetToBoolRing_forget₂_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	carrier of	—	—
hasForgetToBoolAlg_forget₂_map 📖	mathematical	—	CategoryTheory.Functor.map BoolRing instCategory BoolAlg BoolAlg.instCategory CategoryTheory.HasForget₂.forget₂ RingHom carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing booleanRing RingHom.instFunLike instConcreteCategoryRingHomCarrier BoundedLatticeHom BoolAlg.carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BoolAlg.str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier hasForgetToBoolAlg BoolAlg.ofHom AsBoolAlg instBooleanAlgebraAsBoolAlg RingHom.asBoolAlg Hom.hom	—	—
hasForgetToBoolAlg_forget₂_obj_coe 📖	mathematical	—	BoolAlg.carrier CategoryTheory.Functor.obj BoolRing instCategory BoolAlg BoolAlg.instCategory CategoryTheory.HasForget₂.forget₂ RingHom carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing booleanRing RingHom.instFunLike instConcreteCategoryRingHomCarrier BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BoolAlg.str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier hasForgetToBoolAlg AsBoolAlg	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext

BoolRing.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	2 math math: BoolRing.hom_ext_iff, BoolRing.hasForgetToBoolAlg_forget₂_map
hom' 📖	CompOp	3 math math: BoolRing.Iso.mk_hom_hom', BoolRing.Iso.mk_inv_hom', ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

BoolRing.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom_hom' 📖	mathematical	—	BoolRing.Hom.hom' CategoryTheory.Iso.hom BoolRing BoolRing.instCategory RingHomClass.toRingHom RingEquiv BoolRing.carrier Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing BoolRing.booleanRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
mk_inv_hom' 📖	mathematical	—	BoolRing.Hom.hom' CategoryTheory.Iso.inv BoolRing BoolRing.instCategory RingHomClass.toRingHom RingEquiv BoolRing.carrier Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing BooleanRing.toCommRing BoolRing.booleanRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingEquiv.symm	—	—

(root)

Definitions

Name	Category	Theorems
BoolRing 📖	CompData	8 math math: BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, BoolRing.Iso.mk_hom_hom', BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, BoolRing.Iso.mk_inv_hom', BoolAlg.hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, boolRingCatEquivBoolAlg_inverse, BoolRing.hasForgetToBoolAlg_forget₂_map
boolRingCatEquivBoolAlg 📖	CompOp	2 math math: boolRingCatEquivBoolAlg_functor, boolRingCatEquivBoolAlg_inverse
instBooleanAlgebraCarrierToBddLatToBddDistLat 📖	CompOp	—
instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boolRingCatEquivBoolAlg_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor BoolRing BoolAlg BoolRing.instCategory BoolAlg.instCategory boolRingCatEquivBoolAlg CategoryTheory.forget₂ RingHom BoolRing.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing BoolRing.booleanRing RingHom.instFunLike BoolRing.instConcreteCategoryRingHomCarrier BoundedLatticeHom BoolAlg.carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BoolAlg.str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier BoolRing.hasForgetToBoolAlg	—	—
boolRingCatEquivBoolAlg_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse BoolRing BoolAlg BoolRing.instCategory BoolAlg.instCategory boolRingCatEquivBoolAlg CategoryTheory.forget₂ BoundedLatticeHom BoolAlg.carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BoolAlg.str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier RingHom BoolRing.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring BooleanRing.toCommRing BoolRing.booleanRing RingHom.instFunLike BoolRing.instConcreteCategoryRingHomCarrier BoolAlg.hasForgetToBoolRing	—	—

---

← Back to Index