Theorems · Theorem · group theory
Monoid.PushoutI.NormalWord.prod_smul_empty
∀ {ι : 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 φ} [inst_2 : DecidableEq ι]
[inst_3 : (i : ι) → DecidableEq (G i)] (w : Monoid.PushoutI.NormalWord d),
w.prod • Monoid.PushoutI.NormalWord.empty = w- Defined in
- Mathlib.GroupTheory.PushoutI
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
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
- MonoidHomstatement and proof · cited by 3,629
- one_smulproof · cited by 1,374
- MonoidHom.rangeproof · cited by 314
- SemigroupAction.mul_smulproof · cited by 291
- Monoid.PushoutI.NormalWord.Transversalstatement and proof · cited by 45
- Monoid.CoprodI.Word.fstIdxproof · cited by 30
- Monoid.PushoutIstatement and proof · cited by 30
- Monoid.PushoutI.NormalWordstatement and proof · cited by 29
- Monoid.PushoutI.NormalWord.Transversal.setproof · cited by 20
- Monoid.PushoutI.ofproof · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- Monoid.PushoutI.NormalWord.equivproof · cited by 1