Mathlib Map

Theorems · Definition · order theory

AsBoolAlg

Type u_4 → Type u_4

Type synonym to view a Boolean ring as a Boolean algebra.

Defined in
Mathlib.Algebra.Ring.BooleanRing
Cited by
28 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.

ofBoolAlg · cited by 16ofBoolAlgtoBoolAlg · cited by 13toBoolAlgRingHom.asBoolAlg · cited by 4RingHom.asBoolAlgRingEquiv.asBoolRingAsBoolAlg · cited by 2RingEquiv.asBoolRingAsBoo…OrderIso.asBoolAlgAsBoolRing · cited by 2OrderIso.asBoolAlgAsBoolR…ofBoolAlg_symmDiff · cited by 1ofBoolAlg_symmDiffBoolRing.hasForgetToBoolAlg_forget₂_map · cited by 0BoolRing.hasForgetToBoolA…BoolRing.hasForgetToBoolAlg_forget₂_obj_coe · cited by 0BoolRing.hasForgetToBoolA…RingEquiv.asBoolRingAsBoolAlg_apply · cited by 0RingEquiv.asBoolRingAsBoo…RingEquiv.asBoolRingAsBoolAlg_symm_apply · cited by 0RingEquiv.asBoolRingAsBoo…toBoolAlg_add · cited by 0toBoolAlg_addtoBoolAlg_add_add_mul · cited by 0toBoolAlg_add_add_mulofBoolAlg_bot · cited by 0ofBoolAlg_botofBoolAlg_compl · cited by 0ofBoolAlg_complofBoolAlg_inf · cited by 0ofBoolAlg_infAsBoolAlgCITED 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.