module module

`IndisputableMonolith.Ethics.Virtues.NormalForm`

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

declarations in this module (31)

inductive Primitive L18
def primitiveOrderList L24
lemma primitive_mem_order L31
lemma primitiveOrderList_nodup L34
structure MicroMove L39
structure NormalForm L47
def pairList L57
lemma pairList_mem L60
lemma pairList_nodup L65
def rowMoves L70
def toMoves L76
def aggCoeff L80
theorem ofMicroMoves_zero_outside L87
theorem ofMicroMoves_nontrivial L110
def ofMicroMoves L118
theorem rowMoves_pair L129
theorem rowMoves_mem_of_coeff_ne_zero L142
theorem aggCoeff_rowMoves_aux_theorem L157
theorem aggCoeff_rowMoves_aux_axiom L319
lemma aggCoeff_rowMoves_aux L329
lemma aggCoeff_rowMoves L340
theorem aggCoeff_rowMoves_of_ne L350
lemma aggCoeff_append L368
theorem aggCoeff_flatMap L375
lemma sumCoeffs_toMoves L405
lemma mem_toMoves_of_coeff_ne_zero L420
lemma pair_mem_toMoves_map L430
theorem of_toMoves L442
theorem pairList_eq_filtered_range_theorem L468
theorem pairList_eq_filtered_range_axiom L500
lemma pairList_eq_filtered_range L505