Theorems · Definition · group theory
HNNExtension.con
(G : Type u_1) → [inst : Group G] → (A B : Subgroup G) → ↥A ≃* ↥B → Con (Monoid.Coprod G (Multiplicative ℤ))
The relation we quotient the coproduct by to form an HNNExtension.
- Defined in
- Mathlib.GroupTheory.HNNExtension
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- MulEquivstatement and proof · cited by 1,142
- Multiplicativestatement and proof · cited by 875
- Multiplicative.ofAddproof · cited by 237
- Constatement · cited by 152
- Monoid.Coprodstatement and proof · cited by 109
- Monoid.Coprod.inlproof · cited by 48
- Monoid.Coprod.inrproof · cited by 47
- conGenproof · cited by 23
Cited by5
Results whose statement or proof uses this declaration.
- HNNExtensionproof · cited by 26
- HNNExtension.ofproof · cited by 20
- HNNExtension.tproof · cited by 20
- HNNExtension.liftproof · cited by 5
- HNNExtension.t_mul_ofproof · cited by 2