Theorems · Theorem · group theory
pow_mem
∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : SetLike A M] [SubmonoidClass A M] {S : A} {x : M},
x ∈ S → ∀ (n : ℕ), x ^ n ∈ S- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- MonoidSetLikeSubmonoidClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- SetLikestatement and proof · cited by 1,084
- SubmonoidClassstatement and proof · cited by 60
Cited by46
Results whose statement or proof uses this declaration.
- Subalgebra.pow_memproof · cited by 19
- zpow_memproof · cited by 8
- Submonoid.pow_memproof · cited by 6
- Subgroup.strictWidthInfty_pos_iffproof · cited by 5
- IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparableproof · cited by 4
- Subgroup.pow_memproof · cited by 4
- Ideal.spanIntNorm_localizationproof · cited by 3
- Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_memproof · cited by 2
- Polynomial.comp_C_mul_X_eq_zero_iffproof · cited by 2
- SubmonoidClass.mk_powstatement · cited by 2
- IsLocalization.under_map_of_isPrimary_disjointproof · cited by 2