quotientToQuotientRangePowQuotSucc_mk

English

There is a surjective map from the quotient to the codomain quotient arising in ramification context; every element in the codomain quotient has a preimage in the domain quotient.

Русский

Существует суръекционная карта между квотиентами в контексте разветвления; каждый элемент кодомонды имеет предобраз.

LaTeX

$$quotientToQuotientRangePowQuotSucc_surjective p P hi a_mem a_notMem$$

Lean4

theorem quotientToQuotientRangePowQuotSucc_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
    quotientToQuotientRangePowQuotSucc p P a_mem (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩ :=
  quotientToQuotientRangePowQuotSuccAux_mk p P a_mem x

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