English
Adjusting the proof of smul_mem' while keeping the same carrier yields the same Submodule.
Русский
Изменение доказательства closure под действием умножения на скаляр не меняет подмодуль, если носитель остаётся тем же.
LaTeX
$$$\\{ p \\ with\\ smul\\_mem' := h \\} = p$$$
Lean4
instance (priority := 100) :
CanLift (Set M) (Submodule R M) (↑)
(fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x}, x ∈ s → r • x ∈ s)
where
prf s
h :=
⟨{ carrier := s
zero_mem' := h.1
add_mem' := h.2.1
smul_mem' := h.2.2 }, rfl⟩
