Algebraic structure on locally constant functions #
This file puts algebraic structure (Group
, AddGroup
, etc)
on the type of locally constant functions.
FunLike.coe
as an AddMonoidHom
.
Instances For
FunLike.coe
as a MonoidHom
.
Instances For
The constant-function embedding, as an additive monoid hom.
Instances For
The constant-function embedding, as a multiplicative monoid hom.
Instances For
Characteristic functions are locally constant functions taking x : X
to 1
if x ∈ U
,
where U
is a clopen set, and 0
otherwise.
Instances For
The constant-function embedding, as a ring hom.
Instances For
FunLike.coe
as a RingHom
.
Instances For
FunLike.coe
as a linear map.
Instances For
FunLike.coe
as an AlgHom
.
Instances For
Evaluation as an AddMonoidHom
Instances For
Evaluation as a MonoidHom
Instances For
Evaluation as a linear map
Instances For
Evaluation as a RingHom
Instances For
Evaluation as an AlgHom
Instances For
LocallyConstant.comap
as an AddHom
.
Instances For
LocallyConstant.comap
as a MulHom
.
Instances For
LocallyConstant.comap
as an AddMonoidHom
.
Instances For
LocallyConstant.comap
as a MonoidHom
.
Instances For
LocallyConstant.comap
as a linear map.
Instances For
LocallyConstant.comap
as a RingHom
.
Instances For
LocallyConstant.comap
as an AlgHom
Instances For
LocallyConstant.congrLeft
as an AddEquiv
.
Instances For
LocallyConstant.congrLeft
as a MulEquiv
.
Instances For
LocallyConstant.congrLeft
as a linear equivalence.
Instances For
LocallyConstant.congrLeft
as a RingEquiv
.
Instances For
LocallyConstant.congrLeft
as an AlgEquiv
.