module module

`IndisputableMonolith.Loom.Core`

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

used by (2)

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

IndisputableMonolith.Loom.CertificateData module_import
IndisputableMonolith.Loom.Grammar module_import

declarations in this module (106)

abbrev Word L48
abbrev Config L51
def consRed L58
def reduceWord L64
def isReduced L69
def invWord L76
def conjWord L81
theorem reduceWord_cons L83
theorem invWord_cons L86
theorem isReduced_cons_cons L88
theorem isReduced_tail L91
theorem isReduced_consRed L99
theorem isReduced_reduceWord L113
def frameGen L122
def wellFormed L126
structure Mat L135
theorem eq_of L144
def one L154
def mul L156
def det L160
def adj L164
def tr L166
def trN L170
theorem mul_assoc' L172
theorem one_mul' L176
theorem mul_one' L180
theorem mul_def L192
theorem one_def L193
theorem det_mul L195
theorem det_one L200
theorem adj_mul L207
theorem adj_adj L211
theorem tr_adj L215
theorem tr_mul_comm L220
theorem mul_adj_of_det_one L225
theorem adj_mul_of_det_one L234
def cj L244
theorem adj_cj L248
theorem adj_one L251
theorem cj_mul L253
theorem tr_cj L259
def comm L268
theorem comm_cj L270
theorem det_adj L275
theorem tr_comm_symm L285
theorem trN_comm_symm L291
theorem trN_comm_adj L297
abbrev Table L311
def entryOk L313
def matAt L322
theorem entryOk_one L327
theorem entryOk_matAt L329
def letterMat L339
theorem det_letterMat L344
theorem letterMat_mul_neg L359
def evalWord L381
def evalConfig L385
theorem evalWord_cons L387
theorem evalWord_singleton L390
theorem evalWord_append L393
theorem det_evalWord L399
theorem letterMat_neg L408
theorem evalWord_invWord L419
theorem evalWord_consRed L427
theorem evalWord_reduceWord L440
abbrev Subst L453
def getWord L455
def substLetter L460
def substWord L465
theorem substWord_cons L469
def substConfig L472
def tableOfSubst L477
theorem ok_tableOfSubst L480
theorem matAt_tableOfSubst L494
theorem evalWord_substLetter L505
theorem evalWord_substWord L520
def insertNat L531
def sortNat L536
def pairTraces L543
def invariantOf L549

… and 26 more