`compose_left_id`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
domain: Foundation
line: 62 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts on GitHub at line 62.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  59  apply Subtype.ext
  60  ring
  61
  62theorem compose_left_id (a : FrequencyRatio) :
  63    strictMusicRealization.compose strictMusicRealization.one a = a := by
  64  show (⟨1 * a.1, _⟩ : FrequencyRatio) = a
  65  apply Subtype.ext
  66  simp
  67
  68end MusicRich
  69
  70/-! ## Biology -/
  71
  72namespace BiologyRich
  73
  74open Biology
  75
  76theorem lineageCost_zero_iff (a b : LineageState) :
  77    lineageCost a b = 0 ↔ a = b := by
  78  unfold lineageCost
  79  by_cases h : a = b
  80  · simp [h]
  81  · simp [h]
  82
  83def lineageCost_decidable (a b : LineageState) : Decidable (a = b) :=
  84  inferInstance
  85
  86theorem reproduce_assoc (a b c : LineageState) :
  87    reproduce (reproduce a b) c = reproduce a (reproduce b c) := by
  88  unfold reproduce
  89  congr 1
  90  exact Nat.add_assoc _ _ _
  91
  92theorem reproduce_left_id (a : LineageState) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.