IndisputableMonolith.RecogSpec.Core

declarations in this module (26)

• structure Ledger L11
• structure Bridge L17
• structure UnitsEqv L21
• structure DimlessPack L28
• structure AbsolutePack L38
• def phiSubfield L47
• def PhiClosed L52
• lemma mem L58
• lemma self L60
• lemma of_rat L64
• lemma zero L68
• lemma one L71
• lemma add L74
• lemma sub L78
• lemma neg L82
• lemma mul L85
• lemma inv L89
• lemma div L92
• lemma pow L96
• lemma pow_self L99
• lemma inv_self L102
• lemma inv_pow_self L105
• lemma of_nat L108
• lemma half L111
• structure UniversalDimless L118
• def Matches L132