English
If c is a composition of m and hmn is an equality m = n, then c.cast hmn is a composition of n, obtained by transporting c along hmn; both the total sum and the block structure are preserved up to equality.
Русский
Если c — композиция m и задано равенство m = n, то c.cast hmn является композицияn, получаемая перенесением c вдоль hmn; сумма блоков и структура сохраняются (с учетом равенства).
LaTeX
$$$c:\\,\\mathrm{cast}\\;hmn\\;:\\mathrm{Composition}(m) \\to \\mathrm{Composition}(n)\\quad\\text{with}\\quad \\mathrm{blocks\\_sum}(c.cast\\;hmn) = \\mathrm{blocks\\_sum}(c).$$$
Lean4
/-- Change `n` in `(c : Composition n)` to a propositionally equal value. -/
@[simps]
protected def cast (c : Composition m) (hmn : m = n) : Composition n
where
__ := c
blocks_sum := c.blocks_sum.trans hmn
