theorem proved term proof

`totalRecoveryCost_double`

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

formal statement (Lean)

  73theorem totalRecoveryCost_double (n : ℕ) :
  74    totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n := by

Term-mode proof.

  75  unfold totalRecoveryCost
  76  push_cast
  77  ring
  78
  79/-! ## §4. Master certificate -/
  80

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

cryptography_one_statement in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use
rSCryptographicBoundCert in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use

Lean names referenced from this declaration's body.

totalRecoveryCost in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use