Theorems · Theorem · group theory
Subgroup.mem_closure_range_iff
∀ {M : Type u_1} [inst : CommGroup M] {ι : Type u_2} {f : ι → M} {x : M},
x ∈ Subgroup.closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2- Defined in
- Mathlib.Algebra.Group.Subgroup.Finsupp
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- Set.rangestatement and proof · cited by 4,705
- Subgroupstatement · cited by 3,593
- CommGroupstatement and proof · cited by 990
- Finsupp.supportproof · cited by 828
- Set.mem_range_selfproof · cited by 328
- Finsupp.prodstatement and proof · cited by 231
- Subgroup.closurestatement and proof · cited by 196
- Subgroup.toSubmonoidproof · cited by 114
- Subgroup.subset_closureproof · cited by 53
- zpow_memproof · cited by 8
Cited by1
Results whose statement or proof uses this declaration.
- Subgroup.mem_closure_range_iff_of_fintypeproof · cited by 1