instNatPow

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.instNatPow

English

Exponentiation in the quotient corresponds to exponentiation in the base ring: [a]^n = [a^n].

Русский

Возведение в степень в кольце-остатке эквивалентно возведению в степень в исходном кольце: [a]^n = [a^n].

LaTeX

$$$[a]^n = [a^n]$$$

Lean4

instance : NatPow (RingQuot r) :=
  ⟨fun x n ↦ npow r n x⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru