instance instZeroBool_provenance : Zero Bool

Equations

• instZeroBool_provenance = { zero := false }

instance instAddBool_provenance : Add Bool

Equations

• instAddBool_provenance = { add := or }

instance instOneBool_provenance : One Bool

Equations

• instOneBool_provenance = { one := true }

instance instMulBool_provenance : Mul Bool

Equations

• instMulBool_provenance = { mul := and }

instance instSubBool_provenance : Sub Bool

Equations

• instSubBool_provenance = { sub := fun (x1 x2 : Bool) => x1 && !x2 }

instance instCommSemiringBool_provenance : CommSemiring Bool

Equations

• One or more equations did not get rendered due to their size.

instance instSemiringWithMonusBool : SemiringWithMonus Bool

Equations

• One or more equations did not get rendered due to their size.

theorem Bool.absorptive : _root_.absorptive Bool

theorem Bool.idempotent : _root_.idempotent Bool

theorem Bool.mul_sub_left_distributive : _root_.mul_sub_left_distributive Bool

theorem Bool.homomorphism_from_BoolFunc {X : Type} : ∃ (ν : SemiringWithMonusHom Bool (BoolFunc X)), Function.Injective fun (x : Bool) => ν.toRingHom x

Injective m-semiring homomorphism from Bool to Bool[X]