Theorems · Theorem · group theory

Monoid.PushoutI.NormalWord.cons.congr_simp

∀ {ι : 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 φ} {i : ι} (g g_1 : G i) (e_g : g = g_1)
  (w w_1 : Monoid.PushoutI.NormalWord d) (e_w : w = w_1) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  Monoid.PushoutI.NormalWord.cons g w hmw hgr = Monoid.PushoutI.NormalWord.cons g_1 w_1 ⋯ ⋯

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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
Subgroupstatement · cited by 3,593
MonoidHom.rangestatement and proof · cited by 314
Monoid.PushoutI.NormalWord.Transversalstatement and proof · cited by 45
Monoid.CoprodI.Word.fstIdxstatement and proof · cited by 30
Monoid.PushoutI.NormalWordstatement and proof · cited by 29
Monoid.PushoutI.NormalWord.toWordstatement and proof · cited by 18
Monoid.PushoutI.NormalWord.consstatement and proof · cited by 7

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.