extendIdealTo_eq — Mathlib

English

If r ∈ I_y, the extended map φ evaluated at r equals the value of the maximal extension at r · y, i.e., φ(r) = (extensionOfMax i f).toLinearPMap ⟨r · y, hr⟩.

Русский

Если r ∈ I_y, то φ(r) равно значению максимального расширения на r · y: φ(r) = (extensionOfMax i f).toLinearPMap ⟨r · y, hr⟩.

LaTeX

$$$ ExtendIdealTo(i,f,h,y)(r) = (extensionOfMax(i,f)).toLinearPMap \\langle r \\cdot y, hr \\rangle $$$

Lean4

theorem extendIdealTo_eq (h : Module.Baer R Q) {y : N} (r : R) (hr : r • y ∈ (extensionOfMax i f).domain) :
    ExtensionOfMaxAdjoin.extendIdealTo i f h y r = (extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩ := by
  simp only [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h _ _ hr, ExtensionOfMaxAdjoin.idealTo,
    LinearMap.coe_mk, AddHom.coe_mk]

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