def definition def or abbrev

`all`

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

formal statement (Lean)

  67def all : List GreekMode :=

proof body

Definition body.

  68  [.Ionian, .Aeolian, .Mixolydian, .Lydian, .Dorian, .Phrygian, .Locrian]
  69

used by (40)

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

actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all_length in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all_nodup in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
defectDist_quasi_triangle_local in IndisputableMonolith.Algebra.CostAlgebra decl_use
windowSums_shift_equivariant in IndisputableMonolith.Algebra.CostAlgebra decl_use
F2Power in IndisputableMonolith.Algebra.F2Power decl_use
weight_zero_iff in IndisputableMonolith.Algebra.F2Power decl_use
antisymmetric_implies_balance in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
Cycle in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
DoubleEntryAlgebra in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
LedgerPage in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
MoralLedger in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
PotentialFunction in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
PhiInt in IndisputableMonolith.Algebra.PhiRing decl_use
PhiRingObj in IndisputableMonolith.Algebra.RecognitionCategory decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
all_length in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
cross_cousin_count in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
cross_cousin_half in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
KinshipGraphCohomologyCert in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
kinship_one_statement in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
KinshipSystem in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
nontrivial in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
trivial_not_nontrivial in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
AllConstantsDerived in IndisputableMonolith.Astrophysics.MassToLight decl_use
H_RSZeroParameterStatus in IndisputableMonolith.Astrophysics.MassToLight decl_use
ml_derivation_complete in IndisputableMonolith.Astrophysics.MassToLight decl_use

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
GreekMode in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use