abbrev definition def or abbrev

`Word`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  14abbrev Word := List Ribbon

proof body

Definition body.

  15
  16end Ribbons
  17end Masses
  18end IndisputableMonolith
  19
  20

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

ell in IndisputableMonolith.Masses.Ribbons decl_use
massCanonFromWord in IndisputableMonolith.Masses.Ribbons decl_use
normalForm in IndisputableMonolith.Masses.Ribbons decl_use
rewriteOnce in IndisputableMonolith.Masses.Ribbons decl_use
ringSeq in IndisputableMonolith.Masses.Ribbons decl_use
rungFrom in IndisputableMonolith.Masses.Ribbons decl_use
torsion8 in IndisputableMonolith.Masses.Ribbons decl_use
winding in IndisputableMonolith.Masses.Ribbons decl_use
Word in IndisputableMonolith.Masses.Ribbons decl_use
Primitive in IndisputableMonolith.Masses.SectorPrimitive decl_use

depends on (3)

Lean names referenced from this declaration's body.

Ribbon in IndisputableMonolith.Masses.Ribbons decl_use
Word in IndisputableMonolith.Masses.Ribbons decl_use
Ribbon in IndisputableMonolith.Masses.Ribbons.Word decl_use