cast_rev — Mathlib

English

Casting across equalities commutes with reversal: if n = m, then i.rev.cast n m = (i.cast n m).rev for i ∈ Fin(n).

Русский

Перекрытие (cast) при равенстве размерностей commuting с разворотом: если n = m, то i.rev.cast h = (i.cast h).rev.

LaTeX

$$$\forall i:\mathrm{Fin}(n),\forall h:\, n=m,\ i.rev.cast(h) = (i.cast(h)).rev.$$$

Lean4

theorem cast_rev (i : Fin n) (h : n = m) : i.rev.cast h = (i.cast h).rev := by subst h; simp

Похожие утверждения