eval₂_congr — Mathlib

English

A repeated variant of eval₂ congruence: if f=g, s=t, φ=ψ then eval₂ f s φ = eval₂ g t ψ.

Русский

Повторная форма сопоставления eval₂: если f=g, s=t и φ=ψ, то eval₂ f s φ = eval₂ g t ψ.

LaTeX

$$$ f = g \\Rightarrow s = t \\Rightarrow φ = ψ \\Rightarrow eval\\_2 f s φ = eval\\_2 g t ψ $$$

Lean4

theorem eval₂_congr {R S : Type*} [Semiring R] [Semiring S] {f g : R →+* S} {s t : S} {φ ψ : R[X]} :
    f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ := by rintro rfl rfl rfl; rfl

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