mk_reindex_fin_cast — Mathlib

English

Specialized equality for fin-congruence reindexings in the graded monoid.

Русский

Специализированное равенство для реиндексации через fin-congr в градуированной моноде.

LaTeX

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

Lean4

@[simp]
theorem mk_reindex_fin_cast {n m : ℕ} (h : n = m) (x : ⨂[R]^n M) :
    GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m (PiTensorProduct.reindex R (fun _ ↦ M) (finCongr h) x) =
      GradedMonoid.mk n x :=
  by rw [finCongr_eq_equivCast, mk_reindex_cast h]

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