mk_reindex_cast — Mathlib

English

Special case of mk_reindex_cast for Fin 1 and Fin n when h relates n and m.

Русский

Особый случай mk_reindex_cast для Fin 1 и Fin n при relation h между n и m.

LaTeX

$$$ mk\_\{A := \; (⨂[R]^i) M\} m (PiTensorProduct.reindex R (fun _ ↦ M) (finCongr h) x) = mk\_n x $$$

Lean4

@[simp]
theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : ⨂[R]^n M) :
    GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m
        (PiTensorProduct.reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg Fin h) x) =
      GradedMonoid.mk n x :=
  Eq.symm (PiTensorProduct.gradedMonoid_eq_of_reindex_cast h rfl)

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