quotientToQuotientRangePowQuotSuccAux_mk

English

There exists a canonical way to realize a lifted element in the auxiliary quotient as a quotient of a suitable submodule, compatible with the map structure.

Русский

Существует канонический способ представить элемент в вспомогательном квотиенте как частный фактор подмодуля и совместим с отображениями.

LaTeX

$$quotientToQuotientRangePowQuotSuccAux p P a_mem x = Submodule.Quotient.mk ⟨_, _⟩$$

Lean4

theorem quotientToQuotientRangePowQuotSuccAux_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
    quotientToQuotientRangePowQuotSuccAux p P a_mem (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩ :=
  by apply Quotient.map'_mk''

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