Pulling back rings along injective maps, and pushing them forward along surjective maps #
Pullback a LeftDistribClass
instance along an injective function.
Pullback a RightDistribClass
instance along an injective function.
Pullback a Distrib
instance along an injective function.
Instances For
A type endowed with -
and *
has distributive negation, if it admits an injective map that
preserves -
and *
to a type which has distributive negation.
Instances For
Pullback a NonUnitalNonAssocSemiring
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalSemiring
instance along an injective function.
Instances For
Pullback a NonAssocSemiring
instance along an injective function.
Equations
Instances For
Pullback a Semiring
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalNonAssocRing
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalRing
instance along an injective function.
Equations
Instances For
Pullback a NonAssocRing
instance along an injective function.
Equations
Instances For
Pullback a Ring
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalNonAssocCommSemiring
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalCommSemiring
instance along an injective function.
Equations
Instances For
Pullback a CommSemiring
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalNonAssocCommRing
instance along an injective function.
Equations
Instances For
Pullback a NonUnitalCommRing
instance along an injective function.
Equations
Instances For
Pullback a CommRing
instance along an injective function.
Equations
Instances For
Pushforward a LeftDistribClass
instance along a surjective function.
Pushforward a RightDistribClass
instance along a surjective function.
Pushforward a Distrib
instance along a surjective function.
Instances For
A type endowed with -
and *
has distributive negation, if it admits a surjective map that
preserves -
and *
from a type which has distributive negation.
Instances For
Pushforward a NonUnitalNonAssocSemiring
instance along a surjective function.
See note [reducible non-instances].
Equations
Instances For
Pushforward a NonUnitalSemiring
instance along a surjective function.
Instances For
Pushforward a NonAssocSemiring
instance along a surjective function.
Equations
Instances For
Pushforward a Semiring
instance along a surjective function.
Equations
Instances For
Pushforward a NonUnitalNonAssocRing
instance along a surjective function.
Equations
Instances For
Pushforward a NonUnitalRing
instance along a surjective function.
Equations
Instances For
Pushforward a NonAssocRing
instance along a surjective function.
Equations
Instances For
Pushforward a Ring
instance along a surjective function.
Equations
Instances For
Pushforward a NonUnitalNonAssocCommSemiring
instance along a surjective function.
Equations
Instances For
Pushforward a NonUnitalCommSemiring
instance along a surjective function.
Equations
Instances For
Pushforward a CommSemiring
instance along a surjective function.
Equations
Instances For
Pushforward a NonUnitalNonAssocCommRing
instance along a surjective function.
Equations
Instances For
Pushforward a NonUnitalCommRing
instance along a surjective function.
Equations
Instances For
Pushforward a CommRing
instance along a surjective function.