Theorems · Theorem · group theory

Monoid.PushoutI.NormalWord.ext_smul

∀ {ι : 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₁ w₂ : Monoid.PushoutI.NormalWord d} (i : ι),
  Monoid.CoprodI.of ((φ i) w₁.head) • w₁.toWord = Monoid.CoprodI.of ((φ i) w₂.head) • w₂.toWord → w₁ = w₂

Defined in: Mathlib.GroupTheory.PushoutI
Cited by: 1 results in Mathlib
Foundations: Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group Group DecidableEq DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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

DFunLike.coestatement and proof · cited by 62,936
Groupstatement and proof · cited by 6,238
MonoidHomstatement and proof · cited by 3,629
one_smulproof · cited by 1,374
SemigroupAction.mul_smulproof · cited by 291
inv_mul_cancelproof · cited by 107
Monoid.CoprodI.Wordstatement and proof · cited by 55
Monoid.CoprodIstatement and proof · cited by 52
Monoid.PushoutI.NormalWord.Transversalstatement and proof · cited by 45
Monoid.CoprodI.ofstatement and proof · cited by 45
Monoid.CoprodI.Word.toListproof · cited by 39
Monoid.PushoutI.NormalWordstatement and proof · cited by 29

Cited by1

Results whose statement or proof uses this declaration.

Monoid.PushoutI.NormalWord.cons_eq_smulproof · cited by 1