def definition def or abbrev

`offDiagEntries`

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

formal statement (Lean)

  94def offDiagEntries : ℕ := offDiagSize * offDiagSize

Definition body.

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

CrossPatternMatrixCert in IndisputableMonolith.CrossDomain.CrossPatternMatrix decl_use
offDiagEntries_eq in IndisputableMonolith.CrossDomain.CrossPatternMatrix decl_use
offDiag_is_two_fourth in IndisputableMonolith.CrossDomain.CrossPatternMatrix decl_use

Lean names referenced from this declaration's body.