comapEquiv_coe — Mathlib

English

The underlying function of comapEquiv f is exactly the comap f map on functions.

Русский

Базовая функция comapEquiv f совпадает с отображением comap f на функций.

LaTeX

$$$\\big(\\text{comapEquiv } f : (\\tau \\to R) \\to (\\sigma \\to R)\\big) = \\operatorname{comap} f$$$

Lean4

@[simp]
theorem comapEquiv_coe (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R) : (comapEquiv f : (τ → R) → σ → R) = comap f :=
  rfl

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