`IndisputableMonolith.Constants.RSUnitsHelpers`

IndisputableMonolith/Constants/RSUnitsHelpers.lean · 11 lines · 1 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Constants
   6
   7@[simp] lemma c_mul_tau0_eq_ell0 (U : RSUnits) : U.c * U.tau0 = U.ell0 := U.c_ell0_tau0
   8
   9end Constants
  10end IndisputableMonolith
  11

source mirrored from github.com/jonwashburn/shape-of-logic