Documentation Verification Report

Rearrangement

📁 Source: Mathlib/Algebra/Order/Rearrangement.lean

Statistics

Metric	Count
Definitions	0
Theorems `sum_comp_perm_mul_eq_sum_mul_iff`, `sum_comp_perm_smul_eq_sum_smul_iff`, `sum_mul_eq_sum_mul_comp_perm_iff`, `sum_mul_le_sum_comp_perm_mul`, `sum_mul_le_sum_mul_comp_perm`, `sum_mul_lt_sum_comp_perm_mul_iff`, `sum_mul_lt_sum_mul_comp_perm_iff`, `sum_smul_comp_perm_eq_sum_smul_iff`, `sum_smul_le_sum_comp_perm_smul`, `sum_smul_le_sum_smul_comp_perm`, `sum_smul_lt_sum_comp_perm_smul_iff`, `sum_smul_lt_sum_smul_comp_perm_iff`, `sum_comp_perm_mul_eq_sum_mul_iff`, `sum_comp_perm_smul_eq_sum_smul_iff`, `sum_mul_eq_sum_mul_comp_perm_iff`, `sum_mul_le_sum_comp_perm_mul`, `sum_mul_le_sum_mul_comp_perm`, `sum_mul_lt_sum_comp_perm_mul_iff`, `sum_mul_lt_sum_mul_comp_perm_iff`, `sum_smul_comp_perm_eq_sum_smul_iff`, `sum_smul_le_sum_comp_perm_smul`, `sum_smul_le_sum_smul_comp_perm`, `sum_smul_lt_sum_comp_perm_smul_iff`, `sum_smul_lt_sum_smul_comp_perm_iff`, `sum_comp_perm_mul_eq_sum_mul_iff`, `sum_comp_perm_mul_le_sum_mul`, `sum_comp_perm_mul_lt_sum_mul_iff`, `sum_comp_perm_smul_eq_sum_smul_iff`, `sum_comp_perm_smul_le_sum_smul`, `sum_comp_perm_smul_lt_sum_smul_iff`, `sum_mul_comp_perm_eq_sum_mul_iff`, `sum_mul_comp_perm_le_sum_mul`, `sum_mul_comp_perm_lt_sum_mul_iff`, `sum_smul_comp_perm_eq_sum_smul_iff`, `sum_smul_comp_perm_le_sum_smul`, `sum_smul_comp_perm_lt_sum_smul_iff`, `sum_comp_perm_mul_eq_sum_mul_iff`, `sum_comp_perm_mul_le_sum_mul`, `sum_comp_perm_mul_lt_sum_mul_iff`, `sum_comp_perm_smul_eq_sum_smul_iff`, `sum_comp_perm_smul_le_sum_smul`, `sum_comp_perm_smul_lt_sum_smul_iff`, `sum_mul_comp_perm_eq_sum_mul_iff`, `sum_mul_comp_perm_le_sum_mul`, `sum_mul_comp_perm_lt_sum_mul_iff`, `sum_smul_comp_perm_eq_sum_smul_iff`, `sum_smul_comp_perm_le_sum_smul`, `sum_smul_comp_perm_lt_sum_smul_iff`	48
Total	48

Antivary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_comp_perm_mul_eq_sum_mul_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_comp_perm_smul_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_smul_eq_sum_smul_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff` `antivaryOn` `Finset.mem_univ` `Finset.coe_univ`
`sum_mul_eq_sum_mul_comp_perm_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_comp_perm_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_le_sum_comp_perm_mul` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_le_sum_comp_perm_smul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_le_sum_mul_comp_perm` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_le_sum_smul_comp_perm` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_lt_sum_comp_perm_mul_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_lt_sum_comp_perm_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_lt_sum_mul_comp_perm_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_lt_sum_smul_comp_perm_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_smul_comp_perm_eq_sum_smul_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff` `antivaryOn` `Finset.mem_univ` `Finset.coe_univ`
`sum_smul_le_sum_comp_perm_smul` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AntivaryOn.sum_smul_le_sum_comp_perm_smul` `antivaryOn` `Finset.mem_univ`
`sum_smul_le_sum_smul_comp_perm` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AntivaryOn.sum_smul_le_sum_smul_comp_perm` `antivaryOn` `Finset.mem_univ`
`sum_smul_lt_sum_comp_perm_smul_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff` `antivaryOn` `Finset.mem_univ` `Finset.coe_univ`
`sum_smul_lt_sum_smul_comp_perm_iff` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff` `antivaryOn` `Finset.mem_univ` `Finset.coe_univ`

AntivaryOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_comp_perm_mul_eq_sum_mul_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_comp_perm_smul_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_smul_eq_sum_smul_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff` `OrderDual.isOrderedAddCancelMonoid` `OrderDual.instPosSMulStrictMono` `dual_right` `monovaryOn_toDual_right`
`sum_mul_eq_sum_mul_comp_perm_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_comp_perm_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_le_sum_comp_perm_mul` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_le_sum_comp_perm_smul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_le_sum_mul_comp_perm` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_le_sum_smul_comp_perm` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_lt_sum_comp_perm_mul_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_lt_sum_comp_perm_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_lt_sum_mul_comp_perm_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_lt_sum_smul_comp_perm_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_smul_comp_perm_eq_sum_smul_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff` `OrderDual.isOrderedAddCancelMonoid` `OrderDual.instPosSMulStrictMono` `dual_right` `monovaryOn_toDual_right`
`sum_smul_le_sum_comp_perm_smul` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`MonovaryOn.sum_comp_perm_smul_le_sum_smul` `OrderDual.isOrderedAddCancelMonoid` `OrderDual.instPosSMulMono` `dual_right`
`sum_smul_le_sum_smul_comp_perm` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`MonovaryOn.sum_smul_comp_perm_le_sum_smul` `OrderDual.isOrderedAddCancelMonoid` `OrderDual.instPosSMulMono` `dual_right`
`sum_smul_lt_sum_comp_perm_smul_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`sum_smul_le_sum_comp_perm_smul` `PosSMulStrictMono.toPosSMulMono` `sum_comp_perm_smul_eq_sum_smul_iff`
`sum_smul_lt_sum_smul_comp_perm_iff` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`sum_smul_le_sum_smul_comp_perm` `PosSMulStrictMono.toPosSMulMono` `sum_smul_comp_perm_eq_sum_smul_iff`

Monovary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_comp_perm_mul_eq_sum_mul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_comp_perm_smul_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_mul_le_sum_mul` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_comp_perm_smul_le_sum_smul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_mul_lt_sum_mul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_comp_perm_smul_lt_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_smul_eq_sum_smul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff` `monovaryOn` `Finset.mem_univ` `Finset.coe_univ`
`sum_comp_perm_smul_le_sum_smul` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MonovaryOn.sum_comp_perm_smul_le_sum_smul` `monovaryOn` `Finset.mem_univ`
`sum_comp_perm_smul_lt_sum_smul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff` `monovaryOn` `Finset.mem_univ` `Finset.coe_univ`
`sum_mul_comp_perm_eq_sum_mul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_comp_perm_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_comp_perm_le_sum_mul` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_comp_perm_le_sum_smul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_comp_perm_lt_sum_mul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`sum_smul_comp_perm_lt_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_smul_comp_perm_eq_sum_smul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff` `monovaryOn` `Finset.mem_univ` `Finset.coe_univ`
`sum_smul_comp_perm_le_sum_smul` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MonovaryOn.sum_smul_comp_perm_le_sum_smul` `monovaryOn` `Finset.mem_univ`
`sum_smul_comp_perm_lt_sum_smul_iff` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff` `monovaryOn` `Finset.mem_univ` `Finset.coe_univ`

MonovaryOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_comp_perm_mul_eq_sum_mul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_comp_perm_smul_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_mul_le_sum_mul` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_comp_perm_smul_le_sum_smul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_mul_lt_sum_mul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_comp_perm_smul_lt_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_comp_perm_smul_eq_sum_smul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `Equiv.Perm.set_support_symm_eq` `eq_iff_eq_cancel_right` `Equiv.Perm.sum_comp'` `sum_smul_comp_perm_eq_sum_smul_iff` `Function.comp_assoc` `Equiv.Perm.inv_def` `Equiv.symm_comp_self` `Equiv.eq_preimage_iff_image_eq` `Set.image_perm` `comp_right` `Equiv.self_comp_symm`
`sum_comp_perm_smul_le_sum_smul` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Equiv.Perm.sum_comp'` `sum_smul_comp_perm_le_sum_smul` `Equiv.Perm.set_support_symm_eq`
`sum_comp_perm_smul_lt_sum_smul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`sum_comp_perm_smul_le_sum_smul` `PosSMulStrictMono.toPosSMulMono` `sum_comp_perm_smul_eq_sum_smul_iff`
`sum_mul_comp_perm_eq_sum_mul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_comp_perm_eq_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_comp_perm_le_sum_mul` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_smul_comp_perm_le_sum_smul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_mul_comp_perm_lt_sum_mul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`sum_smul_comp_perm_lt_sum_smul_iff` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule`
`sum_smul_comp_perm_eq_sum_smul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`not_imp_not` `Mathlib.Tactic.Push.not_forall_eq` `eq_1` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Equiv.Perm.set_support_mul_subset` `Set.union_subset` `Equiv.swap_apply_ne_self_iff` `LT.lt.ne` `LE.le.trans_lt'` `sum_smul_comp_perm_le_sum_smul` `PosSMulStrictMono.toPosSMulMono` `eq_or_ne` `lt_irrefl` `Finset.sum_erase_add` `Finset.mem_erase` `add_assoc` `Finset.sum_congr` `Equiv.swap_apply_right` `Equiv.swap_apply_left` `add_lt_add_of_le_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Eq.le` `Equiv.swap_apply_of_ne_of_ne` `smul_add_smul_lt_smul_add_smul` `LE.le.antisymm` `Equiv.apply_symm_apply` `Eq.subset` `Set.instReflSubset` `Equiv.Perm.set_support_symm_eq`
`sum_smul_comp_perm_le_sum_smul` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLE` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Finset.induction_on_max_value` `eq_or_ne` `Equiv.swap_comp_apply` `Finset.mem_of_mem_insert_of_ne` `Equiv.injective` `Finset.sum_insert` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `subset` `Finset.subset_insert` `Equiv.swap_self` `Equiv.trans_refl` `Equiv.Perm.inv_eq_iff_eq` `Equiv.apply_symm_apply` `Finset.sum_erase_add` `add_comm` `add_assoc` `Equiv.swap_apply_left` `Finset.sum_congr` `add_le_add` `covariant_swap_add_of_covariant_add` `smul_add_smul_le_smul_add_smul'` `Prod.Lex.toLex_le_toLex` `Finset.mem_insert_of_mem` `Finset.mem_insert_self` `LT.lt.le` `Eq.le` `Equiv.swap_apply_of_ne_of_ne` `Equiv.eq_symm_apply` `Finset.mem_erase`
`sum_smul_comp_perm_lt_sum_smul_iff` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instHasSubset` `setOf` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Preorder.toLT` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`sum_smul_comp_perm_le_sum_smul` `PosSMulStrictMono.toPosSMulMono` `sum_smul_comp_perm_eq_sum_smul_iff`

---

← Back to Index