extendIdealTo_is_extension — Mathlib

English

The map extendIdealTo is an extension of idealTo: for every x ∈ R with mem ∈ I_y, extendIdealTo(x) equals idealTo(x, mem). In other words, the maximal extension agrees with the ideal-level map on the ideal.

Русский

Отображение extendIdealTo является расширением idealTo: для каждого x ∈ R при условии mem ∈ I_y значение extendIdealTo(x) совпадает с idealTo ⟨x, mem⟩.

LaTeX

$$$ \\text{extendIdealTo\_is\_extension }(h,y)\\;: \\forall x\\in I_y, \\; \\mathrm{extendIdealTo}(i,f,h,y)(x) = \\mathrm{idealTo}(i,f,y)(x,\\,x\\text{ mem}) $$$

Lean4

theorem extendIdealTo_is_extension (h : Module.Baer R Q) (y : N) :
    ∀ (x : R) (mem : x ∈ ExtensionOfMaxAdjoin.ideal i f y),
      ExtensionOfMaxAdjoin.extendIdealTo i f h y x = ExtensionOfMaxAdjoin.idealTo i f y ⟨x, mem⟩ :=
  (h (ExtensionOfMaxAdjoin.ideal i f y) (ExtensionOfMaxAdjoin.idealTo i f y)).choose_spec

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