Skip to content

Commit

Permalink
feat(Algebra/Polynomial/AlgebraMap): generalize one of the ring in `m…
Browse files Browse the repository at this point in the history
…ap_aeval_eq_aeval_map` to `Semiring` (#14735)

... it is not needed to be commutative.
  • Loading branch information
acmepjz committed Jul 15, 2024
1 parent 08c93a3 commit af10129
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Polynomial/AlgebraMap.lean
Original file line number Diff line number Diff line change
Expand Up @@ -345,7 +345,7 @@ theorem coeff_zero_eq_aeval_zero' (p : R[X]) : algebraMap R A (p.coeff 0) = aeva
simp [aeval_def]
#align polynomial.coeff_zero_eq_aeval_zero' Polynomial.coeff_zero_eq_aeval_zero'

theorem map_aeval_eq_aeval_map {S T U : Type*} [CommSemiring S] [CommSemiring T] [Semiring U]
theorem map_aeval_eq_aeval_map {S T U : Type*} [Semiring S] [CommSemiring T] [Semiring U]
[Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U}
(h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : R[X]) (a : S) :
ψ (aeval a p) = aeval (ψ a) (p.map φ) := by
Expand Down

0 comments on commit af10129

Please sign in to comment.