Commit 2025-08-21 17:19 b29b02bc

View on Github →

chore: deprecate SubsemiringClass.coe_pow (#27635)

Estimated changes

Modified Mathlib/Algebra/Ring/Subsemiring/Defs.lean

deleted theorem SubsemiringClass.coe_pow

Modified Mathlib/Analysis/Normed/Ring/Basic.lean