Structures · Algebra
AddConstMapClass
Typeclass for maps satisfying f (x + a) = f x + b.
Note that a and b are outParams,
so one should not add instances like
[AddConstMapClass F G H a b] : AddConstMapClass F G H (-a) (-b).
- Defined in
- Mathlib.Algebra.AddConstMap.Basic
- Shape
- 5 explicit arguments · adds map_add_const
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- AddConstEquiv
- AddConstMap
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- AddConstMapClass.map_add_zsmul
- AddConstMapClass.map_add_const
- AddConstMapClass.map_add_nsmul
- AddConstMapClass.map_add_nat'
- AddConstMapClass.map_sub_nsmul
- AddConstMapClass.map_nat'
- AddConstMapClass.rel_map_of_Icc
- AddConstMapClass.map_sub_int'
- AddConstMapClass.map_nat_add'
- AddConstMapClass.map_sub_zsmul
- AddConstMapClass.strictMono_iff_Icc
- AddConstMapClass.map_add_nat
- AddConstMapClass.map_int_add'
- AddConstMapClass.map_nat_add
- AddConstMapClass.map_const
- AddConstMapClass.map_zsmul_add
- AddConstMapClass.map_add_int'
- AddConstMapClass.map_sub_const
- AddConstMapClass.map_sub_nat'
- AddConstMapClass.semiconj
- AddConstMapClass.map_const_add
- AddConstMapClass.map_nat
- AddConstMapClass.monotone_iff_Icc
- AddConstMapClass.map_nsmul_add
- AddConstMapClass.strictAnti_iff_Icc
- AddConstMapClass.map_add_ofNat
- AddConstMapClass.map_add_ofNat'
- AddConstMapClass.antitone_iff_Icc
- AddConstMapClass.map_nsmul_const
- AddConstMapClass.map_int_add
- AddConstMapClass.map_fract
- AddConstMapClass.map_zsmul_const
- AddConstMapClass.map_add_int
- AddConstMapClass.map_ofNat
- AddConstMapClass.map_sub_ofNat'
- AddConstMapClass.map_ofNat_add'
- AddConstMapClass.map_one_add
- AddConstMapClass.map_ofNat_add
- AddConstMapClass.map_ofNat'
- AddConstMapClass.map_one
- AddConstMapClass.map_sub_one
- AddConstMapClass.map_add_one
- AddConstMapClass.map_sub_int
Ancestors0
No ancestors.