4.5. LocalMultiplicity.LocalMultiplicity🔗

Jacobians.LocalMultiplicity.LocalMultiplicity — source

IsConstantMap

A function f : X → Y is constant if there is a single value y : Y that f takes everywhere. Packaged as a Prop for use in the indicator definition of the degree stub.

def IsConstantMap {X : Type u} {Y : Type v} (f : X → Y) : Prop