pow_quot

Mathlib.Algebra.RingQuot

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

English

Exponentiation in the quotient matches exponentiation in the base: [a]^n = [a^n].

Русский

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

LaTeX

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

Lean4

theorem pow_quot {a} {n : ℕ} : (⟨Quot.mk _ a⟩ ^ n : RingQuot r) = ⟨Quot.mk _ (a ^ n)⟩ :=
  by
  change npow r _ _ = _
  rw [npow_def]

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

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

Разделы

Аффилиация

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