Diff — Exponentiation

Revision #2320 → #2571 · back to history

modifiedNegative exponents in a monoid2a6bf781248e

Field	From #2320	To #2571
mathlib.decl	DivInvMonoid.zpow	ZPow.zpow
provenance	ai	ai-moderated

modifiedNegative integer exponent in a monoided7436404a32

Field	From #2320	To #2571
mathlib.decl	DivInvMonoid.zpow	ZPow.zpow
provenance	ai	ai-moderated