cast_refl — Mathlib

English

If two elements a,b of GradedMonoid with contents in tensor powers satisfy a.fst = b.fst and their snd-parts are equal after applying cast R M h, then a = b.

Русский

Если два элемента a,b из GradedMonoid удовлетворяют a.fst = b.fst и их snd-части равны после применения cast R M h, то a = b.

LaTeX

$$$a.fst = b.fst \\implies cast R M h a.snd = b.snd \\Rightarrow a = b$$$

Lean4

@[simp]
theorem cast_refl {i} (h : i = i) : cast R M h = LinearEquiv.refl _ _ :=
  (congr_arg (reindex R fun _ ↦ M) <| finCongr_refl h).trans reindex_refl

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