Theorems · Definition · group theory

Monoid.PushoutI.NormalWord.toWord

{ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} → Monoid.PushoutI.NormalWord d → Monoid.CoprodI.Word G

Defined in: Mathlib.GroupTheory.PushoutI
Cited by: 18 results in Mathlib
Foundations: Depth 8 from the axioms · uses no axioms
Assumes: Group Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Groupstatement and proof · cited by 6,238
MonoidHomstatement and proof · cited by 3,629
Monoid.CoprodI.Wordstatement · cited by 55
Monoid.PushoutI.NormalWord.Transversalstatement and proof · cited by 45
Monoid.PushoutI.NormalWordstatement and proof · cited by 29

Cited by22

Results whose statement or proof uses this declaration.

Monoid.PushoutI.NormalWord.prodproof · cited by 9
Monoid.PushoutI.NormalWord.consstatement and proof · cited by 7
Monoid.PushoutI.NormalWord.equivPairproof · cited by 5
Monoid.PushoutI.NormalWord.normalizedstatement · cited by 3
Monoid.PushoutI.NormalWord.prod_consstatement and proof · cited by 2
Monoid.PushoutI.NormalWord.base_smul_eq_smulproof · cited by 2
Monoid.PushoutI.NormalWord.consRecOnstatement and proof · cited by 1
Monoid.PushoutI.NormalWord.cons_eq_smulstatement and proof · cited by 1
Monoid.PushoutI.NormalWord.cons_toListstatement and proof · cited by 1
Monoid.PushoutI.NormalWord.extstatement and proof · cited by 1
Monoid.PushoutI.NormalWord.ext_smulstatement and proof · cited by 1
Monoid.PushoutI.NormalWord.prod_base_smulproof · cited by 1