Documentation

Lean 4 Proof

theorem totalRevenue_one (R_ad R_mp : ℝ) :
    totalRevenue R_ad R_mp 1 = R_mp := by
  unfold totalRevenue; ring

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:109

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file