Commit 2024-03-26 06:36 859f3760

View on Github →

chore(*): migrate from RingHom.map_* to _root_.map_* (#11660) Cherry-picked from #9607

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

deleted theorem AlgHom.map_list_prod

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/Data/MvPolynomial/Basic.lean

Modified Mathlib/Data/Polynomial/Eval.lean

modified theorem Polynomial.comp_C

Modified Mathlib/Data/Rat/BigOperators.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/SetTheory/Game/PGame.lean