Structures · Algebra
IsCancelVAdd
A vector addition is cancellative if it is pointwise injective on the left and right.
A group action is cancellative in this sense if and only if it is free.
See isCancelVAdd_iff_eq_zero_of_vadd_eq for a more familiar condition.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 2 explicit arguments · adds right_cancel'
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- IsCancelVAdd.right_cancel
- IsCancelVAdd.left_cancel
- IsCancelVAdd.eq_zero_of_vadd
- Topology.IsQuotientMap.isAddQuotientCoveringMap_of_properlyDiscontinuousVAdd
- Set.VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd
- IsCancelVAdd.right_cancel'
- Set.VAddAntidiagonal.eq_of_snd_eq_snd
- AddAction.equivAddSubgroupOrbitsQuotientAddGroup
- isAddQuotientCoveringMap_quotientMk_of_properlyDiscontinuousVAdd
- IsCancelVAdd.toIsLeftCancelVAdd
- AddAction.instChartedSpaceQuotient
- AddSubmonoid.instIsCancelVAddSubtypeMem
- SetLike.instIsCancelVAddSubtypeMem
- IsCancelVAdd.stabilizer_eq_bot