Theorems · Definition · group theory
Monoid.PushoutI.con
{ι : Type u_1} →
{G : ι → Type u_2} →
{H : Type u_3} →
[inst : (i : ι) → Monoid (G i)] →
[inst_1 : Monoid H] → ((i : ι) → H →* G i) → Con (Monoid.Coprod (Monoid.CoprodI G) H)The relation we quotient by to form the pushout
- Defined in
- Mathlib.GroupTheory.PushoutI
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- Constatement · cited by 152
- Monoid.Coprodstatement and proof · cited by 109
- Monoid.CoprodIstatement and proof · cited by 52
- Monoid.Coprod.inlproof · cited by 48
- Monoid.Coprod.inrproof · cited by 47
- Monoid.CoprodI.ofproof · cited by 45
- conGenproof · cited by 23
Cited by6
Results whose statement or proof uses this declaration.
- Monoid.PushoutIproof · cited by 30
- Monoid.PushoutI.ofproof · cited by 20
- Monoid.PushoutI.baseproof · cited by 17
- Monoid.PushoutI.liftproof · cited by 4
- Monoid.PushoutI.of_comp_eq_baseproof · cited by 3
- Monoid.PushoutI.hom_extproof · cited by 2