coe_pow_interval — Mathlib

English

The coercion with exponentiation commutes with the interval power: WithBot.some (instHPow.hPow s n) = instHPow.hPow (WithBot.some s) n.

Русский

Переход через коэрцию и возведение в степень commute: WithBot.some (instHPow.hPow s n) = instHPow.hPow (WithBot.some s) n.

LaTeX

$$$\\text{WithBot.some} (\\text{instHPow}.hPow s n) = \\text{instHPow}.hPow (\\text{WithBot.some } s) n$$$

Lean4

@[to_additive]
theorem coe_pow_interval [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] (s : NonemptyInterval α) (n : ℕ) :
    ↑(s ^ n) = (s : Interval α) ^ n :=
  map_pow (⟨⟨(↑), coe_one_interval⟩, coe_mul_interval⟩ : NonemptyInterval α →* Interval α) _
    _
      -- simp can already prove `coe_nsmul_interval`

Похожие утверждения