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.toNatSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul abs instLatticeInt Int.instAddGroup	add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid zsmul NegZeroClass.toNeg Monoid.toNatPow 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 le_refl 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Mathlib.Tactic.Linarith.natCast_nonneg neg_zsmul Nat.cast_one Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst CancelDenoms.mul_subst 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.toNatPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul abs instLatticeInt Int.instAddGroup	mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid zpow InvOneClass.toInv 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 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Mathlib.Tactic.Linarith.natCast_nonneg zpow_neg Nat.cast_one Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst CancelDenoms.mul_subst 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.toNatSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Real.instMul neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	nsmul NegZeroClass.toZero AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Monoid.toNatPow 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.toNatPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid Real.instMul inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	npow InvOneClass.toOne MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass 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