gradedMonoid_eq_of_cast — Mathlib

English

A,b in GradedMonoid with same fst and snd equal after applying cast R M h implies a=b (extensional equality of the graded monoid).

Русский

Для a,b в GradedMonoid одинаковый fst и равенство snd после cast R M h означает a=b (расширяемое равенство градуированного моноида).

LaTeX

$$theorem gradedMonoid_eq_of_cast {a b} (h : a.fst = b.fst) (h2 : cast R M h a.snd = b.snd) : a = b$$

Lean4

@[ext (iff := false)]
theorem gradedMonoid_eq_of_cast {a b : GradedMonoid fun n => ⨂[R] _ : Fin n, M} (h : a.fst = b.fst)
    (h2 : cast R M h a.snd = b.snd) : a = b :=
  by
  refine gradedMonoid_eq_of_reindex_cast h ?_
  rw [cast] at h2
  rw [← finCongr_eq_equivCast, ← h2]

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