def Lean.Grind.ToInt.pow_of_semiring {α : Type u_1} {I : IntInterval} [Semiring α] [ToInt α I] [OfNat α I] [Mul α I] (h₁ : I.isFinite = true) : Pow α I

A ToInt instance on a semiring preserves powers if it preserves numerals and multiplication.

Equations

• ⋯ = ⋯