pylogic.structures.ringlike package¶

Submodules¶

pylogic.structures.ringlike.commutative_ring module¶

class pylogic.structures.ringlike.commutative_ring.CommutativeRIng[source]¶

class pylogic.structures.ringlike.commutative_ring.CommutativeRIng(*args, **kwargs)

Bases: RIng[Z]

classmethod property_times_is_commutative(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[Equals]][source]¶

times_is_commutative: ForallInSet[ForallInSet[Equals]]¶

pylogic.structures.ringlike.crooked_semiring module¶

class pylogic.structures.ringlike.crooked_semiring.CrookedSemirIng[source]¶

class pylogic.structures.ringlike.crooked_semiring.CrookedSemirIng(*args, **kwargs)

Bases: CrookedSemirng[Z]

one: Constant[Z] | Any¶

classmethod property_times_has_identity(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr], one: Any) → And[IsContainedIn, ForallInSet[And[Equals, Equals]]][source]¶

times_has_identity: And[IsContainedIn, ForallInSet[And[Equals, Equals]]]¶

pylogic.structures.ringlike.crooked_semirng module¶

class pylogic.structures.ringlike.crooked_semirng.CrookedSemirng[source]¶

class pylogic.structures.ringlike.crooked_semirng.CrookedSemirng(*args, **kwargs)

Bases: Ringoid, Generic[Z]

plus_has_identity: And[IsContainedIn, ForallInSet[And[Equals, Equals]]]¶

plus_is_associative: ForallInSet[ForallInSet[ForallInSet[Equals]]]¶

classmethod property_plus_has_identity(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], zero: Any) → And[IsContainedIn, ForallInSet[And[Equals, Equals]]][source]¶

classmethod property_plus_is_associative(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[ForallInSet[Equals]]][source]¶

classmethod property_times_is_associative(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[ForallInSet[Equals]]][source]¶

classmethod property_zero_mul_eq_zero(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr], zero: Any) → ForallInSet[And[Equals, Equals]][source]¶

times_is_associative: ForallInSet[ForallInSet[ForallInSet[Equals]]]¶

zero: Constant[Z] | Any¶

zero_mul_eq_zero: ForallInSet[And[Equals, Equals]]¶

pylogic.structures.ringlike.division_ring module¶

class pylogic.structures.ringlike.division_ring.DivisionRIng[source]¶

class pylogic.structures.ringlike.division_ring.DivisionRIng(*args, **kwargs)

Bases: RIng[Z]

have_mul_inverses: ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]]¶

classmethod property_have_mul_inverses(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr], one: Any) → ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]][source]¶

classmethod property_times_latin_square(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]][source]¶

classmethod property_zero_product(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr], zero: Any) → ForallInSet[ForallInSet[Implies[Equals, Or[Equals, Equals]]]][source]¶

times_latin_square: ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]]¶

zero_product: ForallInSet[ForallInSet[Implies[Equals, Or[Equals, Equals]]]]¶

pylogic.structures.ringlike.field module¶

class pylogic.structures.ringlike.field.Field[source]¶

class pylogic.structures.ringlike.field.Field(*args, **kwargs)

Bases: DivisionRIng[Z]

classmethod property_times_is_commutative(set_: Set, times_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[Equals]][source]¶

times_is_commutative: ForallInSet[ForallInSet[Equals]]¶

pylogic.structures.ringlike.left_ringoid module¶

class pylogic.structures.ringlike.left_ringoid.LeftRingoid[source]¶

class pylogic.structures.ringlike.left_ringoid.LeftRingoid(*args, **kwargs)

Bases: _RingoidCommon

A left-ringoid is a set closed under two binary operations + and *, where * left-distributes over +.

is_closed_under_plus: ForallInSet[ForallInSet[IsContainedIn]]¶

is_closed_under_times: ForallInSet[ForallInSet[IsContainedIn]]¶

classmethod property_times_left_dist_over_plus(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], times_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[ForallInSet[Equals]]][source]¶

times_left_dist_over_plus: ForallInSet[ForallInSet[ForallInSet[Equals]]]¶

pylogic.structures.ringlike.nearring module¶

class pylogic.structures.ringlike.nearring.NearrIng[source]¶

class pylogic.structures.ringlike.nearring.NearrIng(*args, **kwargs)

Bases: CrookedSemirIng[Z]

have_add_inverses: ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]]¶

plus_latin_square¶: alias of ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]]

classmethod property_have_add_inverses(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], zero: Any) → ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]][source]¶

classmethod property_plus_latin_square(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]][source]¶

pylogic.structures.ringlike.ordered_field module¶

pylogic.structures.ringlike.right_ringoid module¶

class pylogic.structures.ringlike.right_ringoid.RightRingoid[source]¶

class pylogic.structures.ringlike.right_ringoid.RightRingoid(*args, **kwargs)

Bases: _RingoidCommon

A left-ringoid is a set closed under two binary operations + and *, where * left-distributes over +.

is_closed_under_plus: ForallInSet[ForallInSet[IsContainedIn]]¶

is_closed_under_times: ForallInSet[ForallInSet[IsContainedIn]]¶

classmethod property_times_right_dist_over_plus(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], times_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[ForallInSet[Equals]]][source]¶

times_right_dist_over_plus: ForallInSet[ForallInSet[ForallInSet[Equals]]]¶

pylogic.structures.ringlike.ring module¶

class pylogic.structures.ringlike.ring.RIng[source]¶

class pylogic.structures.ringlike.ring.RIng(*args, **kwargs)

Bases: SemirIng[Z]

have_add_inverses: ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]]¶

plus_latin_square¶: alias of ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]]

classmethod property_have_add_inverses(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], zero: Any) → ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]][source]¶

classmethod property_plus_latin_square(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]][source]¶

pylogic.structures.ringlike.ringoid module¶

pylogic.structures.ringlike.ringoid.RIngoid¶: alias of Ringoid

class pylogic.structures.ringlike.ringoid.Ringoid[source]¶

class pylogic.structures.ringlike.ringoid.Ringoid(*args, **kwargs)

Bases: LeftRingoid, RightRingoid

A ringoid is a set closed under two binary operations + and *, where * distributes over +.

is_closed_under_plus: ForallInSet[ForallInSet[IsContainedIn]]¶

is_closed_under_times: ForallInSet[ForallInSet[IsContainedIn]]¶

classmethod property_times_dist_over_plus(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], times_operation: SpecialInfix[Any, Any, Expr, Expr]) → And[ForallInSet[ForallInSet[ForallInSet[Equals]]], ForallInSet[ForallInSet[ForallInSet[Equals]]]][source]¶

times_dist_over_plus: And[ForallInSet[ForallInSet[ForallInSet[Equals]]], ForallInSet[ForallInSet[ForallInSet[Equals]]]]¶

pylogic.structures.ringlike.rng module¶

class pylogic.structures.ringlike.rng.Rng[source]¶

class pylogic.structures.ringlike.rng.Rng(*args, **kwargs)

Bases: Semirng[Z]

have_add_inverses: ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]]¶

plus_latin_square¶: alias of ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]]

classmethod property_have_add_inverses(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr], zero: Any) → ForallInSet[ExistsUniqueInSet[And[Equals, Equals]]][source]¶

classmethod property_plus_latin_square(set_: Set, plus_operation: SpecialInfix[Any, Any, Expr, Expr]) → ForallInSet[ForallInSet[And[ExistsUniqueInSet[Equals], ExistsUniqueInSet[Equals]]]][source]¶

pylogic.structures.ringlike.semiring module¶

class pylogic.structures.ringlike.semiring.SemirIng[source]¶

class pylogic.structures.ringlike.semiring.SemirIng(*args, **kwargs)