Theorem MvPolynomial.rTensorAlgEquiv_apply

Modification history

2026-07-04 08:56
Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
refactor(Algebra): make `MonoidAlgebra` into a one-field structure (#38714) …
Modified MvPolynomial.rTensorAlgEquiv_applyView on Github →
2024-12-23 15:20
Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
feat(AlgebraicGeometry): `Spec R[X] -> Spec R` is open (#20159)
Added MvPolynomial.rTensorAlgEquiv_applyView on Github →