Theorems · Theorem · group theory
Finset.pow_right_strictMono
∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G},
1 ∈ X → (↑(Subgroup.closure ↑X)).Infinite → StrictMono fun n => X ^ n- Cited by
- 0 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Groupstatement and proof · cited by 6,238
- Set.ofPredproof · cited by 6,101
- Subgroupstatement · cited by 3,593
- StrictMonostatement · cited by 706
- Set.Infinitestatement and proof · cited by 263
- Subgroup.closurestatement and proof · cited by 196
- StrictMonoOnproof · cited by 194
- Finset.coe_singletonproof · cited by 145
- Finset.Nontrivialproof · cited by 53
- Finset.monoidstatement · cited by 20
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.