English
If hs is a linear independence condition on a set s and t is any superset of s, then the extended submodule hs.extend hst is contained in the span of t.
Русский
Если hs задаёт линейную независимость на s, и t содержит s, то расширение hs.extend hst лежит внутри порождающего подпространства span t.
LaTeX
$$$s\\subseteq t\\ ;\\ hs:\\ LinearIndepOn\\ K\\ id\\ s\\ \\Rightarrow\\ s \\subseteq hs.extend\\, (subset\\_univ\\, _)$$$
Lean4
@[simp]
theorem addSubgroupOfClosure_repr_apply (h : A = .closure (Set.range b)) (x : A) (i : ι) :
(b.addSubgroupOfClosure A h).repr x i = b.repr x i :=
by
suffices
Finsupp.mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ (b.addSubgroupOfClosure A h).repr.toLinearMap =
((b.repr : M →ₗ[R] ι →₀ R).restrictScalars ℤ).domRestrict A.toIntSubmodule
by exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
exact (b.addSubgroupOfClosure A h).ext fun _ ↦ by simp
