right_inv — Mathlib

English

The map toFunAlgHom composed with invFun is the identity on A[X].

Русский

Правый обратный: toFunAlgHom ∘ invFun = id на A[X].

LaTeX

$$(toFunAlgHom_R A) (invFun_R A x) = x$$

Lean4

theorem right_inv (x : A[X]) : (toFunAlgHom R A) (invFun R A x) = x :=
  by
  refine Polynomial.induction_on' x ?_ ?_
  · intro p q hp hq
    simp only [invFun_add, map_add, hp, hq]
  · intro n a
    rw [invFun_monomial, Algebra.TensorProduct.tmul_pow, one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul,
        toFunAlgHom_apply_tmul, X_pow_eq_monomial, sum_monomial_index] <;>
      simp

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