LinearLowerBound

📁 Source: Mathlib/Geometry/Group/Growth/LinearLowerBound.lean

Statistics

Metric	Count
Definitions	0
Theorems add_nonneg_card_nsmul, add_one_le_card_pow, nsmul_right_strictMono, nsmul_right_strictMonoOn, nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure, pow_right_strictMono, pow_right_strictMonoOn, pow_ssubset_pow_succ_of_pow_ne_closure	8
Total	8

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_nonneg_card_nsmul 📖	mathematical	Finset instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.Infinite SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure instSetLike	card nsmul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	zero_add zero_nsmul card_zero le_refl LE.le.trans_lt card_lt_card nsmul_right_strictMono
add_one_le_card_pow 📖	mathematical	Finset instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.Infinite SetLike.coe Subgroup Subgroup.instSetLike Subgroup.closure instSetLike	card npow MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	zero_add pow_zero card_one LE.le.trans_lt card_lt_card pow_right_strictMono
nsmul_right_strictMono 📖	mathematical	Finset instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.Infinite SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure instSetLike	StrictMono Nat.instPreorder PartialOrder.toPreorder partialOrder AddMonoid.toNatSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	eq_singleton_or_nontrivial coe_singleton AddSubgroup.closure_singleton_zero Set.Finite.not_infinite Set.finite_singleton coe_nsmul finite_toSet strictMonoOn_univ nsmul_right_strictMonoOn
nsmul_right_strictMonoOn 📖	mathematical	Finset instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Nontrivial	StrictMonoOn Nat.instPreorder PartialOrder.toPreorder partialOrder AddMonoid.toNatSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid setOf Set Set.NSMul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SetLike.coe instSetLike AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure	—	strictMonoOn_of_lt_add_one Nat.instIsSuccArchimedean zero_le Nat.instCanonicallyOrderedAdd zero_nsmul coe_set_eq_zero AddSubgroup.closure_eq_bot_iff Set.Nontrivial.not_subset_singleton Nontrivial.coe add_nsmul Set.nsmul_add_addSubgroupClosure Nonempty.to_set Nontrivial.nonempty nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure
nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure 📖	mathematical	Finset instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Nontrivial	instHasSSubset nsmul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	eq_or_ne zero_nsmul zero_add one_nsmul ssubset_iff_subset_not_subset instIsNonstrictStrictOrderSubsetSSubset zero_subset Nontrivial.not_subset_singleton HasSubset.Subset.ssubset_of_ne instAntisymmSubset nsmul_subset_nsmul_right Mathlib.Tactic.Contrapose.contrapose₄ AddSubgroup.closure_nsmul mem_coe two_nsmul add_mem_add vadd_finset_subset_add eq_of_subset_of_card_le Eq.ge card_vadd_finset eq_neg_vadd_iff mem_neg_vadd_finset_iff add_neg_cancel HasSubset.Subset.antisymm Set.instAntisymmSubset AddSubgroup.subset_closure AddSubgroup.closure_le subset_rfl Set.instReflSubset add_zero add_assoc add_nsmul coe_nsmul zero_mem_nsmul Nontrivial.nsmul one_ne_zero mul_nsmul mul_two
pow_right_strictMono 📖	mathematical	Finset instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.Infinite SetLike.coe Subgroup Subgroup.instSetLike Subgroup.closure instSetLike	StrictMono Nat.instPreorder PartialOrder.toPreorder partialOrder Monoid.toNatPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid	—	eq_singleton_or_nontrivial coe_singleton Subgroup.closure_singleton_one pow_right_strictMonoOn
pow_right_strictMonoOn 📖	mathematical	Finset instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Nontrivial	StrictMonoOn Nat.instPreorder PartialOrder.toPreorder partialOrder Monoid.toNatPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid setOf Set Set.NPow MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SetLike.coe instSetLike Subgroup Subgroup.instSetLike Subgroup.closure	—	strictMonoOn_of_lt_add_one Nat.instIsSuccArchimedean Nat.instCanonicallyOrderedAdd pow_zero Set.Nontrivial.not_subset_singleton Nontrivial.coe pow_add Set.pow_mul_subgroupClosure Nonempty.to_set Nontrivial.nonempty pow_ssubset_pow_succ_of_pow_ne_closure
pow_ssubset_pow_succ_of_pow_ne_closure 📖	mathematical	Finset instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Nontrivial	instHasSSubset npow MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	eq_or_ne pow_zero zero_add pow_one instIsNonstrictStrictOrderSubsetSSubset Nontrivial.not_subset_singleton HasSubset.Subset.ssubset_of_ne instAntisymmSubset pow_subset_pow_right Mathlib.Tactic.Contrapose.contrapose₄ Subgroup.closure_pow mul_mem_mul smul_finset_subset_mul eq_of_subset_of_card_le Eq.ge card_smul_finset eq_inv_smul_iff mul_inv_cancel HasSubset.Subset.antisymm Set.instAntisymmSubset Subgroup.subset_closure Subgroup.closure_le subset_rfl Set.instReflSubset add_zero add_assoc pow_add one_mem_pow Nontrivial.pow one_ne_zero mul_two

---

← Back to Index