Theorems · Theorem · group theory

Monoid.CoprodI.Word.mk.congr_simp

∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (toList toList_1 : List ((i : ι) × M i))
  (e_toList : toList = toList_1) (ne_one : ∀ l ∈ toList, l.snd ≠ 1)
  (chain_ne : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList),
  { toList := toList, ne_one := ne_one, chain_ne := chain_ne } = { toList := toList_1, ne_one := ⋯, chain_ne := ⋯ }

Defined in: Mathlib.GroupTheory.CoprodI
Cited by: 3 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms
Assumes: Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites2

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

Monoidstatement and proof · cited by 3,887
Monoid.CoprodI.Wordstatement · cited by 55

Cited by3

Results whose statement or proof uses this declaration.

Monoid.CoprodI.Word.cons_eq_smulproof · cited by 2
Monoid.PushoutI.NormalWord.extproof · cited by 1
Monoid.CoprodI.NeWord.of_wordproof · cited by 1