Commit 2024-11-11 20:18 33a52a30

View on Github →

chore: move results about the kernel of Polynomial.modByMonicHom earlier (#18883) These need no further imports, and are the only results that use Polynomial.modByMonicHom (or anything else from Algebra.Polynomial.RingDivision) in RingTheory.Polynomial.Basic.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

added theorem Polynomial.ker_modByMonicHom

added theorem Polynomial.mem_ker_modByMonic

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Polynomial.ker_modByMonicHom

deleted theorem Polynomial.mem_ker_modByMonic

Modified Mathlib/RingTheory/Polynomial/Quotient.lean