Commit 2025-09-02 18:54 9d84681b

View on Github →

chore(RingTheory/Localization/Algebra): generalize universes and to CommSemiring (#28642)

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/RingTheory/Localization/Algebra.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

modified theorem Localization.mk_intCast