Structures · Algebra
BooleanRing
A Boolean ring is a ring where multiplication is idempotent.
- Defined in
- Mathlib.Algebra.Ring.BooleanRing
- Shape
- One type argument · adds isIdempotentElem
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every BooleanRing is also a
Concrete types that are instances5
- Bool
- Lat.carrier
- AsBoolRing
- BoolRing.carrier
- PUnit
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- BooleanRing.mul_self
- BooleanRing.add_self
- BooleanRing.sup
- BooleanRing.inf
- RingHom.asBoolAlg
- RingEquiv.asBoolRingAsBoolAlg
- BooleanRing.neg_eq
- BooleanRing.le_sup_inf_aux
- BooleanRing.isIdempotentElem
- BoolRing.ofHom
- ofBoolAlg_symmDiff
- BooleanRing.add_eq_zero'
- RingEquiv.asBoolRingAsBoolAlg_symm_apply
- BooleanRing.toRing
- BooleanRing.toCommRing
- BooleanRing.toBooleanAlgebra
- instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg
- ofBoolAlg_sup
- toBoolAlg_mul
- ofBoolAlg_top
- instBooleanAlgebraAsBoolAlg
- BooleanRing.inf_assoc
- BooleanRing.inf_comm
- BooleanRing.inf_sup_self
- toBoolAlg_one
- BooleanRing.mul_one_add_self
- RingEquiv.asBoolRingAsBoolAlg_apply
- toBoolAlg_add_add_mul
- BooleanRing.le_sup_inf
- BooleanRing.instIdempotentOpHMul
- ofBoolAlg_compl
- ofBoolAlg_inf
- BooleanRing.sub_eq_add
- toBoolAlg_zero
- RingHom.asBoolAlg_toFun
- BoolRing.coe_of
- toBoolAlg_add
- RingHom.asBoolAlg_comp
- BooleanRing.sup_comm
- BooleanRing.mul_add_mul
- ofBoolAlg_mul_ofBoolAlg_eq_left_iff
- BooleanRing.sup_inf_self
- BooleanRing.sup_assoc
- ofBoolAlg_sdiff
- ofBoolAlg_bot
- RingHom.asBoolAlg_id
Ancestors95
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommRing
- CommSemigroup
- CommSemiring
- Distrib
- Dvd
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- Ideal.FiniteHeight
- IntCast
- InvolutiveNeg
- IsJacobsonRing
- IsLeftCancelAdd
- IsRightCancelAdd
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.CommRing
- Lean.Grind.CommSemiring
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocCommRing
- NonAssocCommSemiring
- NonAssocRing
- NonAssocSemiring
- NonUnitalCommRing
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalRing
- NonUnitalSemiring
- Nonempty
- OfNat
- One
- Ring
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- Semiring
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero