English
Equality of the underlying functions of the inverse of a restricted scalars equivalence and the original inverse when viewed as functions.
Русский
Равенство подстановок для обратной стороны ограниченного по скалярам эквивалентности и исходной обратной функции.
LaTeX
$$$$\\operatorname{coe}( (\\operatorname{restrictScalars}_R f)^{-1} ) = \\operatorname{coe}(f^{-1})$$$$
Lean4
theorem span_smul_of_span_eq_top {s : Set S} (hs : span R s = ⊤) (t : Set A) :
span R (s • t) = (span S t).restrictScalars R :=
le_antisymm (span_le.2 fun _x ⟨p, _hps, _q, hqt, hpqx⟩ ↦ hpqx ▸ (span S t).smul_mem p (subset_span hqt)) fun _ hp ↦
closure_induction (hx := hp) (zero_mem _) (fun _ _ _ _ ↦ add_mem) fun s0 y hy ↦
by
refine
span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_ (hs ▸ mem_top : s0 ∈ span R s)
· rw [zero_smul]; apply zero_mem
· intro _ _ _ _; rw [add_smul]; apply add_mem
· intro r s0 _ hy; rw [IsScalarTower.smul_assoc]; exact smul_mem _ r hy
