extendIdealTo_wd' — Mathlib

English

If r is a scalar with r · y = 0, then extendIdealTo(i,f,h,y) maps r to 0. The extension respects annihilators of y.

Русский

Если r · y = 0, то extendIdealTo(i,f,h,y)(r) = 0. Расширение сохраняет нуль-деление по y.

LaTeX

$$$ extendIdealTo\_wd' (h) (y) \\;: \\forall r, (r \\cdot y = 0) \\Rightarrow extendIdealTo(i,f,h,y)(r) = 0 $$$

Lean4

theorem extendIdealTo_wd' (h : Module.Baer R Q) {y : N} (r : R) (eq1 : r • y = 0) :
    ExtensionOfMaxAdjoin.extendIdealTo i f h y r = 0 :=
  by
  have : r ∈ ideal i f y := by
    change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain
    rw [eq1]
    apply Submodule.zero_mem _
  rw [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h y r this]
  dsimp [ExtensionOfMaxAdjoin.idealTo]
  simp only [eq1, ← ZeroMemClass.zero_def, (extensionOfMax i f).toLinearPMap.map_zero]

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