Commit 2025-03-24 15:47 7c6b5f8d

chore: more on rank of localized module (#23095)

• Prove IsBaseChange.(lift_)rank_eq: base change along an injective map of domains preserves rank.
• Split results including IsLocalizedModule.linearIndependent_lift and IsLocalizedModule.(lift_)rank_eq into two: one changes the module, and the other changes the ring.
• Add some results connecting nonZeroDivisors and injectivity of localization to regular elements, towards the resolution of issue #22997.
• Improve FractionRing.liftAlgebra API: remove the redundant [IsDomain R] assumption and add a missing IsScalarTower instance.
• Show that any localization of a CommSemiring without zero-divisors has no zero-divisors, and deprecate noZeroDivisors_of_le_nonZeroDivisors. Golf and remove extraneous conditions from sec_fst_ne_zero.