Commit 2025-04-01 14:16 b663fbed

View on Github →

chore(RingTheory): various api additions (#22920) This PR adds

AlgEquiv.quotientBot and minimal API.
AdjoinRoot.free_of_monic, AdjoinRoot.finite_of_monic and Polynomial versions.
Module.Free.trans

Estimated changes

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

added theorem Module.Free.trans

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem Polynomial.Monic.finite_adjoinRoot

added theorem Polynomial.Monic.finite_quotient

added theorem Polynomial.Monic.free_adjoinRoot

added theorem Polynomial.Monic.free_quotient

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

added def AlgEquiv.quotientBot

added theorem AlgEquiv.quotientBot_mk

added theorem AlgEquiv.quotientBot_symm_mk

modified def RingEquiv.quotientBot

added theorem RingEquiv.quotientBot_mk

added theorem RingEquiv.quotientBot_symm_mk