English
There are internal equalities that relate the constructions in the adjoin extension, ensuring compatibility of the fst and snd components with the original maps, and guaranteeing that addition and scalar action behave as expected on the extended space.
Русский
Внутренние равенства в конструкциях дополняющего расширения обеспечивают совместимость компонент fst и snd с исходными отображениями и корректность операций сложения и скаляра на расширенном пространстве.
LaTeX
$$$ \\text{adjoin\_eqn} : \\text{relations between fst, snd and original maps} $$$
Lean4
theorem extensionOfMax_le (h : Module.Baer R Q) {y : N} : extensionOfMax i f ≤ extensionOfMaxAdjoin i f h y :=
⟨le_sup_left, fun x x' EQ => by
symm
change ExtensionOfMaxAdjoin.extensionToFun i f h _ = _
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero, add_zero]⟩
