cast_eq_cast — Mathlib

English

If h is an equality i=j, then the cast from ⨂^i M to ⨂^j M is equal to a canonical cast induced by congruence through i ↦ ⨂^i M.

Русский

Если h является равенством i=j, то преобразование cast между ⨂^i M и ⨂^j M равно каноническому преобразованию cast, индуцированному эквивалентностью через i ↦ ⨂^i M.

LaTeX

$$cast_R M h = _root_.cast (congrArg (fun i => ⨂[R]^i M) h)$$

Lean4

theorem cast_eq_cast {i j} (h : i = j) : ⇑(cast R M h) = _root_.cast (congrArg (fun i => ⨂[R]^i M) h) :=
  by
  subst h
  rw [cast_refl]
  rfl

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