comapEquiv_symm_coe — Mathlib

English

Let f be an algebra isomorphism f: MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R. Then the inverse of the correspondence comapEquiv f, viewed as a map from σ → R to τ → R, coincides with comap f.symm.

Русский

Пусть f — алгебраическая эквивалентность f: MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R. Тогда обратное отображение comapEquiv f, рассматриваемое как функция (σ → R) → (τ → R), равно comap f.symm.

LaTeX

$$$((\\mathrm{comapEquiv}(f)).\\mathrm{symm} : (\\sigma \\to R) \\to \\tau \\to R) = \\mathrm{comap}(f.\\mathrm{symm})$$$

Lean4

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

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