PluenneckeRuzsa

📁 Source: Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Statistics

Metric	Count
Definitions	0
Theorems card_div_mul_le_card_div_mul_card_mul, card_sub_add_le_card_sub_add_card_add, pluennecke_petridis_inequality_add, pluennecke_petridis_inequality_mul, pluennecke_ruzsa_inequality_nsmul_add, pluennecke_ruzsa_inequality_nsmul_sub, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub, pluennecke_ruzsa_inequality_pow_div, pluennecke_ruzsa_inequality_pow_div_pow_div, pluennecke_ruzsa_inequality_pow_div_pow_mul, pluennecke_ruzsa_inequality_pow_mul, ruzsa_triangle_inequality_addNeg_addNeg_addNeg, ruzsa_triangle_inequality_addNeg_add_add, ruzsa_triangle_inequality_add_addNeg_add, ruzsa_triangle_inequality_add_add_add, ruzsa_triangle_inequality_add_add_negAdd, ruzsa_triangle_inequality_add_sub_add, ruzsa_triangle_inequality_add_sub_sub, ruzsa_triangle_inequality_div_div_div, ruzsa_triangle_inequality_div_mul_div, ruzsa_triangle_inequality_div_mul_mul, ruzsa_triangle_inequality_invMul_invMul_invMul, ruzsa_triangle_inequality_invMul_mul_mul, ruzsa_triangle_inequality_mulInv_mulInv_mulInv, ruzsa_triangle_inequality_mulInv_mul_mul, ruzsa_triangle_inequality_mul_div_div, ruzsa_triangle_inequality_mul_div_mul, ruzsa_triangle_inequality_mul_mulInv_mul, ruzsa_triangle_inequality_mul_mul_invMul, ruzsa_triangle_inequality_mul_mul_mul, ruzsa_triangle_inequality_negAdd_add_add, ruzsa_triangle_inequality_negAdd_negAdd_negAdd, ruzsa_triangle_inequality_sub_add_add, ruzsa_triangle_inequality_sub_add_sub, ruzsa_triangle_inequality_sub_sub_sub	36
Total	36

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_div_mul_le_card_div_mul_card_mul 📖	mathematical	—	card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	div_inv_eq_mul div_eq_mul_inv ruzsa_triangle_inequality_mul_div_div
card_sub_add_le_card_sub_add_card_add 📖	mathematical	—	card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	sub_neg_eq_add sub_eq_add_neg ruzsa_triangle_inequality_add_sub_sub
pluennecke_petridis_inequality_add 📖	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—	induction_on empty_add MulZeroClass.zero_mul MulZeroClass.mul_zero le_refl add_assoc singleton_add_inter AddLeftCancelSemigroup.toIsLeftCancelAdd IsAddUnit.add_neg_cancel_left isAddUnit_singleton insert_eq union_comm union_add sup_sdiff_eq_sup add_le_add_left instAddRightMono inter_subset_right add_subset_add subset_refl instReflSubset inter_subset_left mul_le_mul_left covariant_swap_mul_of_covariant_mul Nat.instMulLeftMono LE.le.trans_eq card_union_le card_sdiff_of_subset add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le card_le_card card_singleton_add tsub_mul LE.total add_mul Distrib.rightDistribClass tsub_le_tsub covariant_swap_add_of_covariant_add mul_add Distrib.leftDistribClass mul_tsub add_comm eq_tsub_of_add_eq card_union_add_card_inter
pluennecke_petridis_inequality_mul 📖	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—	induction_on empty_mul MulZeroClass.zero_mul MulZeroClass.mul_zero mul_assoc singleton_mul_inter LeftCancelSemigroup.toIsLeftCancelMul IsUnit.mul_inv_cancel_left isUnit_singleton insert_eq union_comm union_mul sup_sdiff_eq_sup mul_le_mul_left instMulRightMono inter_subset_right mul_subset_mul subset_refl instReflSubset inter_subset_left covariant_swap_mul_of_covariant_mul Nat.instMulLeftMono LE.le.trans_eq card_union_le card_sdiff_of_subset add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le card_le_card card_singleton_mul tsub_mul LE.total add_mul Distrib.rightDistribClass tsub_le_tsub add_le_add_left covariant_swap_add_of_covariant_add mul_add Distrib.leftDistribClass mul_tsub add_comm eq_tsub_of_add_eq card_union_add_card_inter
pluennecke_ruzsa_inequality_nsmul_add 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv add	—	zero_nsmul sub_zero pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add
pluennecke_ruzsa_inequality_nsmul_sub 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv sub SubNegMonoid.toSub	—	zero_nsmul sub_zero pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub
pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv add	—	mem_erase_of_ne_of_mem Nonempty.ne_empty mem_powerset_self exists_min_image nonempty_iff_ne_empty mem_powerset mem_erase le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.cast_mul Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero ruzsa_triangle_inequality_sub_add_add add_comm mul_le_mul' IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid covariant_swap_mul_of_covariant_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add mul_le_mul_left pow_le_pow_left' Nat.mono_cast card_le_card Nat.cast_pos' NeZero.charZero_one Nonempty.card_pos
pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv	—	card_neg neg_sub' neg_nsmul sub_eq_add_neg pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add
pluennecke_ruzsa_inequality_pow_div 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv div DivInvMonoid.toDiv	—	pow_zero div_one pluennecke_ruzsa_inequality_pow_div_pow_div
pluennecke_ruzsa_inequality_pow_div_pow_div 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv	—	card_inv inv_div' inv_pow div_eq_mul_inv pluennecke_ruzsa_inequality_pow_div_pow_mul
pluennecke_ruzsa_inequality_pow_div_pow_mul 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv mul	—	mem_erase_of_ne_of_mem Nonempty.ne_empty mem_powerset_self exists_min_image nonempty_iff_ne_empty mem_powerset mem_erase le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero ruzsa_triangle_inequality_div_mul_mul mul_comm mul_le_mul' IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid covariant_swap_mul_of_covariant_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add mul_le_mul_left pow_le_pow_left' Nat.mono_cast card_le_card Nat.cast_pos' NeZero.charZero_one Nonempty.card_pos
pluennecke_ruzsa_inequality_pow_mul 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card Finset npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNRat.instDiv mul	—	pow_zero div_one pluennecke_ruzsa_inequality_pow_div_pow_mul
ruzsa_triangle_inequality_addNeg_addNeg_addNeg 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	sub_eq_add_neg ruzsa_triangle_inequality_sub_sub_sub
ruzsa_triangle_inequality_addNeg_add_add 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	card_neg neg_neg ruzsa_triangle_inequality_addNeg_addNeg_addNeg
ruzsa_triangle_inequality_add_addNeg_add 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	sub_eq_add_neg ruzsa_triangle_inequality_add_sub_add
ruzsa_triangle_inequality_add_add_add 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	eq_empty_or_nonempty MulZeroClass.mul_zero add_empty empty_add le_refl mem_erase_of_ne_of_mem Nonempty.ne_empty mem_powerset_self exists_min_image Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero Nat.cast_mul le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_pos NNRat.instNontrivial Nonempty.card_pos mul_div_right_comm add_comm LE.le.trans card_le_card_add_left AddLeftCancelSemigroup.toIsLeftCancelAdd nonempty_iff_ne_empty mem_powerset mem_erase le_trans add_assoc Rat.instIsStrictOrderedRing Nonneg.coe_inv Nonneg.coe_div Nonneg.coe_zpow pluennecke_petridis_inequality_add mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono card_le_card add_subset_add_right zero_le NNRat.instCanonicallyOrderedAdd
ruzsa_triangle_inequality_add_add_negAdd 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg ruzsa_triangle_inequality_addNeg_add_add
ruzsa_triangle_inequality_add_sub_add 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid sub SubNegMonoid.toSub	—	sub_eq_add_neg neg_neg ruzsa_triangle_inequality_negAdd_add_add
ruzsa_triangle_inequality_add_sub_sub 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup sub SubNegMonoid.toSub	—	sub_eq_add_neg card_neg neg_sub' sub_neg_eq_add ruzsa_triangle_inequality_add_add_add
ruzsa_triangle_inequality_div_div_div 📖	mathematical	—	card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid	—	card_product mul_one card_mul_le_card_mul mem_div card_le_card_of_injOn mem_coe mem_bipartiteAbove mk_mem_product div_mem_div div_div_div_cancel_right div_right_injective card_le_one_iff mem_bipartiteBelow
ruzsa_triangle_inequality_div_mul_div 📖	mathematical	—	card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	div_eq_mul_inv ruzsa_triangle_inequality_mul_mul_mul
ruzsa_triangle_inequality_div_mul_mul 📖	mathematical	—	card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	card_inv div_inv_eq_mul ruzsa_triangle_inequality_div_div_div
ruzsa_triangle_inequality_invMul_invMul_invMul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	div_eq_mul_inv card_map mul_comm ruzsa_triangle_inequality_div_div_div
ruzsa_triangle_inequality_invMul_mul_mul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	card_inv inv_inv ruzsa_triangle_inequality_invMul_invMul_invMul
ruzsa_triangle_inequality_mulInv_mulInv_mulInv 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	div_eq_mul_inv ruzsa_triangle_inequality_div_div_div
ruzsa_triangle_inequality_mulInv_mul_mul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	card_inv inv_inv ruzsa_triangle_inequality_mulInv_mulInv_mulInv
ruzsa_triangle_inequality_mul_div_div 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup div DivInvMonoid.toDiv	—	div_eq_mul_inv card_inv inv_div' div_inv_eq_mul ruzsa_triangle_inequality_mul_mul_mul
ruzsa_triangle_inequality_mul_div_mul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid div DivInvMonoid.toDiv	—	div_eq_mul_inv inv_inv ruzsa_triangle_inequality_invMul_mul_mul
ruzsa_triangle_inequality_mul_mulInv_mul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	div_eq_mul_inv ruzsa_triangle_inequality_mul_div_mul
ruzsa_triangle_inequality_mul_mul_invMul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv ruzsa_triangle_inequality_mulInv_mul_mul
ruzsa_triangle_inequality_mul_mul_mul 📖	mathematical	—	card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	eq_empty_or_nonempty MulZeroClass.mul_zero mul_empty empty_mul mem_erase_of_ne_of_mem Nonempty.ne_empty mem_powerset_self exists_min_image Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero Nat.cast_mul le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_pos NNRat.instNontrivial Nonempty.card_pos mul_div_right_comm mul_comm LE.le.trans card_le_card_mul_left LeftCancelSemigroup.toIsLeftCancelMul nonempty_iff_ne_empty mem_powerset mem_erase le_trans mul_assoc Rat.instIsStrictOrderedRing Nonneg.coe_inv Nonneg.coe_div Nonneg.coe_zpow pluennecke_petridis_inequality_mul mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono card_le_card mul_subset_mul_right zero_le NNRat.instCanonicallyOrderedAdd
ruzsa_triangle_inequality_negAdd_add_add 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	card_neg neg_neg ruzsa_triangle_inequality_negAdd_negAdd_negAdd
ruzsa_triangle_inequality_negAdd_negAdd_negAdd 📖	mathematical	—	card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	sub_eq_add_neg map_op_neg map_op_add card_map mul_comm ruzsa_triangle_inequality_sub_sub_sub
ruzsa_triangle_inequality_sub_add_add 📖	mathematical	—	card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	card_neg sub_neg_eq_add ruzsa_triangle_inequality_sub_sub_sub
ruzsa_triangle_inequality_sub_add_sub 📖	mathematical	—	card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	sub_eq_add_neg ruzsa_triangle_inequality_add_add_add
ruzsa_triangle_inequality_sub_sub_sub 📖	mathematical	—	card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	card_product mul_one card_mul_le_card_mul mem_sub card_le_card_of_injOn mem_coe mem_bipartiteAbove mk_mem_product sub_mem_sub sub_sub_sub_cancel_right sub_right_injective card_le_one_iff mem_bipartiteBelow

---

← Back to Index