transitionMap_map_pow — Mathlib

English

For any n and X ∈ AdicCauchySequence, evalₐ I n (mk I R X) equals the quotient of X.val n by I^n.

Русский

Для любого n и X ∈ AdicCauchySequence выполняется evalₐ I n (mk I R X) = Quotient.mk (I^n) (X.val n).

LaTeX

$$evalₐ(I,n)(mk(I,R)X) = Quotient.mk(I^n)(X.val n)$$

Lean4

@[local simp]
theorem transitionMap_map_pow {m n a : ℕ} (hmn : m ≤ n) (x : R ⧸ (I ^ n • ⊤ : Ideal R)) :
    transitionMap I R hmn (x ^ a) = transitionMap I R hmn x ^ a :=
  Quotient.inductionOn' x (fun _ ↦ rfl)

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