coe_pow

Mathlib.RingTheory.Congruence.Defs

URI: https://scilib.ai/kg/mathlib#RingCon.coe_pow

English

The image of a power commutes with the quotient: (↑(x^n) : c.Quotient) = (x : c.Quotient)^n.

Русский

Образ степени в кольце и фактор-гомология согласованы: (↑(x^n)) = (↑x)^n в Quotient.

LaTeX

$$$$\left( ↑(x^n) : c.Quotient \right) = \left( x : c.Quotient \right)^n.$$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (x : R) (n : ℕ) : (↑(x ^ n) : c.Quotient) = (x : c.Quotient) ^ n :=
  rfl

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

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

Разделы

Аффилиация

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