Structures · Algebra
AddRightCancelSemigroup
An AddRightCancelSemigroup is an additive semigroup such that
a + b = c + b implies a = c.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances16
- Real
- Rat
- Filter.Germ
- Matrix
- DomAddAct
- PNat
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Fin
- Lex
- AddOpposite
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by74
- CochainComplex
- ChainComplex
- ChainComplex.of.d
- CochainComplex.of.d
- CochainComplex.next
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalence
- ChainComplex.of_d
- ChainComplex.prev
- ChainComplex.linearYonedaObj
- CochainComplex.of_d
- ChainComplex.of
- HomologicalComplex.coinvariantsTensorObj
- CochainComplex.of
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom
- ComplexShape.instDecidableRelRelDown'
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f
- ComplexShape.instDecidableRelRelUp
- CochainComplex.ofHom
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X
- AddRightCancelSemigroup.toIsRightCancelAdd
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f
- ChainComplex.ofHom
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f
- ComplexShape.instDecidableRelRelDown
- ChainComplex.of.congr_simp
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p
- Colex.instAddRightCancelSemigroup
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f
- Prod.instAddRightCancelSemigroup
- Pi.addRightCancelSemigroup
- Multiplicative.rightCancelSemigroup
- ULift.addRightCancelSemigroup
- ChainComplex.map_chain_complex_of
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f
- Matrix.instAddRightCancelSemigroup
- OrderDual.instAddRightCancelSemigroup
- Function.Injective.addRightCancelSemigroup
- ChainComplex.of_d_ne
- ChainComplex.of.d.congr_simp
- CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f
- CochainComplex.of.d.congr_simp
- Filter.Germ.instAddRightCancelSemigroup
- instQFactorsThroughHomotopyDown
- DomAddAct.instAddRightCancelSemigroupOfAddOpposite
- ComplexShape.instDecidableRelRelUp'
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f
- ChainComplex.of_X