def definition def or abbrev

`shiftedCompose`

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

formal statement (Lean)

 225def shiftedCompose (A B : ShiftedCarrier) : ShiftedCarrier := by

proof body

Definition body.

 226  refine ⟨2 * A.1 * B.1, ?_⟩
 227  nlinarith [A.2, B.2]
 228
 229instance : Mul ShiftedCarrier := ⟨shiftedCompose⟩
 230
 231/-- The identity element `1/2` for the shifted monoid. -/

depends on (7)

Lean names referenced from this declaration's body.

ShiftedCarrier in IndisputableMonolith.Algebra.CostAlgebra decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use