extendIdealTo_wd — Mathlib

English

If r • y = r' • y, then the two extensions φ(r) and φ(r') coincide. The extension respects the linear relation induced by y.

Русский

Если r · y = r' · y, то extendIdealTo(i,f,h,y)(r) = extendIdealTo(i,f,h,y)(r').

LaTeX

$$$ \\forall r,r'\\; (r \\cdot y = r' \\cdot y) \\Rightarrow ExtendIdealTo(i,f,h,y)(r) = ExtendIdealTo(i,f,h,y)(r') $$$

Lean4

theorem extendIdealTo_wd (h : Module.Baer R Q) {y : N} (r r' : R) (eq1 : r • y = r' • y) :
    ExtensionOfMaxAdjoin.extendIdealTo i f h y r = ExtensionOfMaxAdjoin.extendIdealTo i f h y r' :=
  by
  rw [← sub_eq_zero, ← map_sub]
  convert ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _
  rw [sub_smul, sub_eq_zero, eq1]

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