rTensorAlgEquiv_apply — Mathlib

English

The algebraic equivalence rTensorAlgEquiv acts on x by sending it to rTensorAlgHom x; i.e., the two ways of representing the same element agree.

Русский

Эквивалентность rTensorAlgEquiv действует на x так, что x maps to rTensorAlgHom x; тождественность двух представлений выполняется.

LaTeX

$$$rTensorAlgEquiv\\; x = rTensorAlgHom\\; x$$$

Lean4

@[simp]
theorem rTensorAlgEquiv_apply (x : (MvPolynomial σ S) ⊗[R] N) : rTensorAlgEquiv x = rTensorAlgHom x :=
  by
  rw [← AlgHom.coe_coe, ← AlgEquiv.toAlgHom_eq_coe]
  congr 1
  ext _ d <;> simpa [rTensorAlgEquiv] using rTensor_apply_tmul_apply _ _ d

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