Theorems · Theorem · group theory
PresentedGroup.generated_by
∀ {α : Type u_1} (rels : Set (FreeGroup α)) (H : Subgroup (PresentedGroup rels)),
(∀ (j : α), PresentedGroup.of j ∈ H) → ∀ (x : PresentedGroup rels), x ∈ H- Defined in
- Mathlib.GroupTheory.PresentedGroup
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Subgroupstatement and proof · cited by 3,593
- HasQuotient.Quotientproof · cited by 2,301
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
- FreeGroupstatement and proof · cited by 132
- Subgroup.toSubmonoidproof · cited by 114
- OneMemClass.one_memproof · cited by 87
- FreeGroup.ofproof · cited by 39
- Subgroup.normalClosureproof · cited by 35
- Subgroup.mul_memproof · cited by 30
- PresentedGroupstatement and proof · cited by 21
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.