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 SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.Infinite SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure	card Finset nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	zero_add zero_nsmul card_zero instReflLe LE.le.trans_lt card_lt_card nsmul_right_strictMono
add_one_le_card_pow 📖	mathematical	Finset SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.Infinite SetLike.coe Subgroup Subgroup.instSetLike Subgroup.closure	card Finset npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	zero_add pow_zero card_one instReflLe LE.le.trans_lt card_lt_card pow_right_strictMono
nsmul_right_strictMono 📖	mathematical	Finset SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.Infinite SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.closure	StrictMono Finset Nat.instPreorder PartialOrder.toPreorder partialOrder AddMonoid.toNSMul 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 SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Nontrivial	StrictMonoOn Finset Nat.instPreorder PartialOrder.toPreorder partialOrder AddMonoid.toNSMul addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid setOf Set Set.NSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid 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 SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Nontrivial	Finset instHasSSubset nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid 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 SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.Infinite SetLike.coe Subgroup Subgroup.instSetLike Subgroup.closure	StrictMono Finset Nat.instPreorder PartialOrder.toPreorder partialOrder Monoid.toPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid	—	eq_singleton_or_nontrivial coe_singleton Subgroup.closure_singleton_one pow_right_strictMonoOn
pow_right_strictMonoOn 📖	mathematical	Finset SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Nontrivial	StrictMonoOn Finset Nat.instPreorder PartialOrder.toPreorder partialOrder Monoid.toPow monoid DivInvMonoid.toMonoid Group.toDivInvMonoid setOf Set Set.NPow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid 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 SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Nontrivial	Finset instHasSSubset npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid 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