SmallTripling

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

Statistics

Metric	Count
Definitions	0
Theorems small_alternating_nsmul_of_small_tripling, small_alternating_pow_of_small_tripling, small_nsmul_of_small_tripling, small_pow_of_small_tripling	4
Total	4

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small_alternating_nsmul_of_small_tripling 📖	mathematical	Real Real.instLE Real.instNatCast card Finset AddMonoid.toNSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul abs instLatticeInt Int.instAddGroup	Real Real.instLE Real.instNatCast card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid zsmul NegZeroClass.toNeg Real.instMul Monoid.toPow Real.instMonoid	—	ne_of_gt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat abs_zero Int.instAddLeftMono zero_ne_one eq_empty_or_nonempty zsmul_empty List.sum_replicate nsmul_empty Nat.cast_zero MulZeroClass.mul_zero instReflLe one_le_of_le_mul_right₀ MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Nonempty.card_pos LE.le.trans' Nat.cast_le card_le_card_nsmul Nat.instAtLeastTwoHAddOfNat OfNat.ofNat_ne_zero Nat.instCharZero pow_mul add_zero add_assoc le_self_pow₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_right₀ abs_eq Int.instIsOrderedAddMonoid zero_le_one Int.instZeroLEOneClass Fin.forall_iff_succ IsEmpty.forall_iff Fin.isEmpty' one_zsmul le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le succ_nsmul zero_nsmul zero_add Mathlib.Tactic.Linarith.sub_neg_of_lt mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Mathlib.Tactic.Linarith.natCast_nonneg neg_zsmul Nat.cast_one Mathlib.Tactic.Linarith.without_one_mul Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.CancelDenoms.mul_subst Mathlib.Tactic.CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow neg_add_rev card_neg pow_succ' pow_zero mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add succ_nsmul'
small_alternating_pow_of_small_tripling 📖	mathematical	Real Real.instLE Real.instNatCast card Finset Monoid.toPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul abs instLatticeInt Int.instAddGroup	Real Real.instLE Real.instNatCast card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid zpow InvOneClass.toInv Real.instMul Monoid.toPow Real.instMonoid	—	ne_of_gt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat abs_zero Int.instAddLeftMono eq_empty_or_nonempty empty_zpow List.prod_replicate empty_pow Nat.cast_zero MulZeroClass.mul_zero instReflLe one_le_of_le_mul_right₀ MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Nonempty.card_pos LE.le.trans' card_le_card_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat pow_mul mul_one le_self_pow₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_right₀ Int.instIsOrderedAddMonoid Int.instZeroLEOneClass Fin.isEmpty' zpow_one le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le pow_succ pow_zero one_mul Mathlib.Tactic.Linarith.sub_neg_of_lt mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Mathlib.Tactic.Linarith.natCast_nonneg zpow_neg Nat.cast_one Mathlib.Tactic.Linarith.without_one_mul Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.CancelDenoms.mul_subst Mathlib.Tactic.CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow card_inv pow_succ' Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add
small_nsmul_of_small_tripling 📖	mathematical	Real Real.instLE Real.instNatCast card Finset AddMonoid.toNSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Real Real.instLE Real.instNatCast card Finset nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul Monoid.toPow Real.instMonoid	—	eq_or_eq_neg_of_abs_eq one_zsmul neg_zsmul List.sum_replicate add_zero succ_nsmul' zero_nsmul abs_one IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing
small_pow_of_small_tripling 📖	mathematical	Real Real.instLE Real.instNatCast card Finset Monoid.toPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Real Real.instLE Real.instNatCast card Finset npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul Monoid.toPow Real.instMonoid	—	eq_or_eq_neg_of_abs_eq zpow_one zpow_neg List.prod_replicate mul_one pow_succ' pow_zero abs_one IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing

---

← Back to Index