Structures · Algebra
IsOrderedCancelVAdd
An ordered cancellative vector addition is an ordered vector addition that is cancellative.
- Defined in
- Mathlib.Algebra.Order.AddTorsor
- Shape
- 2 explicit arguments · adds le_of_vadd_le_vadd_left, le_of_vadd_le_vadd_right
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- Set.VAddAntidiagonal.finite_of_isPWO
- HahnSeries.SummableFamily.smul
- HahnModule.coeff_smul
- VAdd.vadd_lt_vadd_of_lt_of_le
- HahnModule.support_smul_subset_vadd_support
- HahnSeries.SummableFamily.coeff_smul
- HahnSeries.SummableFamily.smul_hsum
- HahnModule.coeff_single_zero_smul
- HahnModule.zero_smul'
- HahnModule.coeff_smul_left
- HahnModule.coeff_smul_right
- HahnModule.coeff_single_smul_vadd
- Set.VAddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
- HahnSeries.SummableFamily.smul_toFun
- HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq
- HahnModule.support_smul_subset_vadd_support'
- HahnSeries.SummableFamily.hsum_smul_module
- HahnSeries.SummableFamily.isPWO_iUnion_support_prod_smul
- HahnSeries.SummableFamily.finite_co_support_prod_smul
- Finset.vaddAntidiagonal_min_vadd_min
- HahnSeries.SummableFamily.smul_eq
- HahnModule.orderTop_vAdd_le_orderTop_smul
- IsOrderedCancelVAdd.le_of_vadd_le_vadd_left
- HahnModule.single_zero_smul_eq_smul
- IsOrderedCancelVAdd.le_of_vadd_le_vadd_right
- HahnModule.instIsScalarTowerHahnSeries_1
- HahnModule.instDistribSMul
- HahnSeries.SummableFamily.instModule
- HahnModule.instModule
- HahnModule.add_smul
- HahnModule.smul_add
- HahnModule.one_smul'
- VAdd.vadd_lt_vadd_of_le_of_lt
- HahnModule.instSMul
- Finset.isPWO_support_vaddAntidiagonal
- instIsCancelVAddOfIsOrderedCancelVAdd
- HahnSeries.SummableFamily.instSMul_1
- HahnSeries.SummableFamily.smul.congr_simp
- HahnSeries.SummableFamily.smul_apply
- instContravariantClassHVAddLeOfIsOrderedCancelVAdd
- IsOrderedCancelVAdd.toIsOrderedVAdd
- HahnModule.SMulCommClass
- HahnModule.instSMulZeroClass