module module

`IndisputableMonolith.Verification.DimensionalRigidity`

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 (8)

theorem rather L28
def dimC L41
def dimHbar L44
def dimG L47
def dimMatrix L50
theorem dimMatrix_det L54
theorem no_dimensionless_combination L61
theorem si_values_not_derivable_from_pure_numbers L74