transitionMap_ideal_mk — Mathlib

English

For natural numbers m ≤ n, the transition map commutes with taking powers: transitionMap(I,R,hmn) (x^a) = (transitionMap(I,R,hmn) x)^a.

Русский

Для натуральных чисел m ≤ n имеет место переходная карта, сохраняющая возведение в степень: transitionMap(I,R,hmn)(x^a) = (transitionMap(I,R,hmn) x)^a.

LaTeX

$$$transitionMap(I,R,hmn)(x^a) = transitionMap(I,R,hmn)(x)^a$$$

Lean4

@[local simp]
theorem transitionMap_ideal_mk {m n : ℕ} (hmn : m ≤ n) (x : R) :
    transitionMap I R hmn (Ideal.Quotient.mk (I ^ n • ⊤ : Ideal R) x) = Ideal.Quotient.mk (I ^ m • ⊤ : Ideal R) x :=
  rfl

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