English
If e is a linear equivalence, then the repr of Basis.ofEquivFun e matches e on every x and i: (Basis.ofEquivFun e).repr x i = e x i.
Русский
Если e — линейное эквивалентное отображение, то представление Basis.ofEquivFun e совпадает с e на каждой паре x, i: (Basis.ofEquivFun e).repr x i = e x i.
LaTeX
$$$$ (Basis.ofEquivFun e).repr x i = e x i $$$$
Lean4
/-- An unbundled version of `repr_eq_iff` -/
theorem repr_apply_eq (f : M → ι → R) (hadd : ∀ x y, f (x + y) = f x + f y)
(hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x) (f_eq : ∀ i, f (b i) = Finsupp.single i 1) (x : M) (i : ι) :
b.repr x i = f x i :=
by
let f_i : M →ₗ[R] R :=
{ toFun x := f x i
map_add' _ _ := by rw [hadd, Pi.add_apply]
map_smul' _ _ := by simp [hsmul, Pi.smul_apply] }
have : Finsupp.lapply i ∘ₗ ↑b.repr = f_i := by
refine b.ext fun j => ?_
change b.repr (b j) i = f (b j) i
rw [b.repr_self, f_eq]
calc
b.repr x i = f_i x := by {
rw [← this]
rfl
}
_ = f x i := rfl
