From 3c19986341931bd0504f8e17977a78a7ee6832c7 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 20 Jun 2026 10:31:53 +0800 Subject: [PATCH] init commit --- Mathlib/RingTheory/Polynomial/Basic.lean | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean index c186c48bb63ee7..efa4f23011e935 100644 --- a/Mathlib/RingTheory/Polynomial/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Basic.lean @@ -763,17 +763,8 @@ theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} : (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s) have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C := by apply ringHom_ext - · intro - simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C, - AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans, - Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_C, - renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply] - · intro - simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X, - AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans, - Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_X, - renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply, Sum.swap_inr, - Equiv.Set.sumCompl_apply_inl] + · simp [eqv] + · simp [eqv] apply_fun (· p) at this simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, Function.comp_apply] at this