equiv — Mathlib

English

Equality of cons with smul: cons g w hmw hgr equals the smul form of head with g.

Русский

Равенство cons с умножением: cons g w hmw hgr равно smul‑форме головы с g.

LaTeX

$$$$cons(g,w,hmw,hgr) = of (\phi := \phi) i g \cdot w.$$$$

Lean4

/-- The equivalence between normal forms and elements of the pushout -/
noncomputable def equiv : PushoutI φ ≃ NormalWord d :=
  { toFun := fun g => g • .empty
    invFun := fun w => w.prod
    left_inv := fun g => by simp only [prod_smul, prod_empty, mul_one]
    right_inv := fun w => prod_smul_empty w }

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