of — Mathlib · SciLib

English

Two HahnModule elements are equal if their underlying HahnSeries representations agree coefficientwise after applying the isomorphism of the type.

Русский

Два элемента HahnModule равны, если их представления через гамильтоновую серию совпадают по коэффициентам.

LaTeX

$$$x = y \iff ((\mathrm{of}\, \mathrm{R}).symm\, x).\mathrm{coeff} = ((\mathrm{of}\, \mathrm{R}).symm\, y).\mathrm{coeff}$$$

Lean4

/-- The casting function to the type synonym. -/
def of (R : Type*) [SMul R V] : HahnSeries Γ V ≃ HahnModule Γ R V :=
  Equiv.refl _

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