Mathlib Map

Theorems · Inductive type · order theory

BoolRing

Type (u + 1)

The category of Boolean rings.

Defined in
Mathlib.Algebra.Category.BoolRing
Cited by
15 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

BoolRing.carrier · cited by 13BoolRing.carrierBoolRing.Hom.hom' · cited by 4Hom.hom'BoolRing.Hom.hom · cited by 3Hom.homBoolRing.Hom.ext · cited by 2Hom.extBoolRing.Iso.mk · cited by 2Iso.mkboolRingCatEquivBoolAlg · cited by 2boolRingCatEquivBoolAlgBoolRing.Hom · cited by 2BoolRing.HomBoolRing.hom_ext · cited by 1BoolRing.hom_extBoolRing.ofHom · cited by 1BoolRing.ofHomBoolRing.of.inj · cited by 1of.injBoolRing.of.noConfusion · cited by 1of.noConfusionBoolRing.ctorIdx · cited by 0BoolRing.ctorIdxBoolRing.hasForgetToBoolAlg_forget₂_map · cited by 0BoolRing.hasForgetToBoolA…BoolRing.hasForgetToBoolAlg_forget₂_obj_coe · cited by 0BoolRing.hasForgetToBoolA…BoolRing.hom_ext_iff · cited by 0BoolRing.hom_ext_iffBoolRingCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by33

Results whose statement or proof uses this declaration.