Commit 2024-11-13 14:41 6806f160

View on Github →

feat(RingTheory/Localization/*): add IsLocalization.algEquivOfAlgEquiv and other results (#18661)

  • MulEquivClass.map_nonZeroDivisors: MulEquiv preserves non-zero divisors
  • IsLocalization.algEquivOfAlgEquiv: generalizes IsLocalization.ringEquivOfRingEquiv
  • rename IsFractionRing.fieldEquivOfRingEquiv -> IsFractionRing.ringEquivOfRingEquiv as it does not require field assumption anymore
  • IsFractionRing.algEquivOfAlgEquiv: generalize IsFractionRing.ringEquivOfRingEquiv
  • IsLocalization.liftAlgHom, IsFractionRing.liftAlgHom: AlgHom version of lift
  • generalize FractionRing.algEquiv to ring case
  • remove IsDomain assumption as much as possible. This makes the left hand side of mk'_eq_zero_iff_eq_zero not a simp normal form, so it's removed from simp lemmas.

Estimated changes