realize_termOfFreeCommRing — Mathlib

English

For p in the free commutative ring on α and v: α→R, the interpretation of the term of p equals the lift of p by v.

Русский

Для p из свободного коммутативного кольца на α и отображения v: α→R, интерпретация терма p равна отображению-подъему (lift) p по v.

LaTeX

$$$ (\\text{termOfFreeCommRing } p).realize\\, v = \\text{FreeCommRing.lift } v\, p $$$

Lean4

@[simp]
theorem realize_termOfFreeCommRing (p : FreeCommRing α) (v : α → R) :
    (termOfFreeCommRing p).realize v = FreeCommRing.lift v p :=
  by
  rw [termOfFreeCommRing]
  conv_rhs => rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]
  induction Classical.choose (exists_term_realize_eq_freeCommRing p) with
  | var _ => simp
  | func f a ih => cases f <;> simp [ih]

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