(** * The law that a sum in an exponent is a product *) (** ** [yⁿ⁺ᵐ ≅ yⁿ × yᵐ] *) Require ExponentialLaws.Law2.Functors. Require ExponentialLaws.Law2.Law. Include ExponentialLaws.Law2.Functors. Include ExponentialLaws.Law2.Law.
(** * The law that a sum in an exponent is a product *) (** ** [yⁿ⁺ᵐ ≅ yⁿ × yᵐ] *) Require ExponentialLaws.Law2.Functors. Require ExponentialLaws.Law2.Law. Include ExponentialLaws.Law2.Functors. Include ExponentialLaws.Law2.Law.