gradedMonoid_eq_of_cast — Mathlib

English

Two elements a and b of the graded monoid of modular forms are equal if their first components agree and their second components agree after casting by the appropriate equality h.

Русский

Два элемента a и b градуированного моноида модульных форм равны, если совпадают их первые компоненты и после приведения по соответствующему равенству h совпадают их вторые компоненты.

LaTeX

$$$a,b \in \mathrm{GradedMonoid}(\mathrm{ModularForm}\, \Gamma),\ a.fst = b.fst,\ mcast(h)\,a.snd = b.snd \Rightarrow a=b$.$$

Lean4

@[ext (iff := false)]
theorem gradedMonoid_eq_of_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMonoid (ModularForm Γ)} (h : a.fst = b.fst)
    (h2 : mcast h a.snd = b.snd) : a = b := by
  obtain ⟨i, a⟩ := a
  obtain ⟨j, b⟩ := b
  cases h
  exact congr_arg _ h2

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