def definition def or abbrev

`apply`

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

formal statement (Lean)

 145@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset

Definition body.

 146
 147/-- Map δ-subgroup to ℝ by composing an affine map with a provided projection to ℤ. -/

Lean names referenced from this declaration's body.