English
If two linear maps agree on all basis vectors, they are equal.
Русский
Если два линейных отображения совпадают на всех базисных векторах, они равны.
LaTeX
$$$$ \forall i, f_1(b_i) = f_2(b_i) \Rightarrow f_1 = f_2 $$$$
Lean4
/-- If `R` and `R'` are isomorphic rings that act identically on a module `M`,
then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.
See also `Basis.algebraMapCoeffs` for the case where `f` is equal to `algebraMap`.
-/
@[simps +simpRhs]
def mapCoeffs (h : ∀ (c) (x : M), f c • x = c • x) : Basis ι R' M :=
by
letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)
haveI : IsScalarTower R' R M :=
{
smul_assoc := fun x y z => by
change (f.symm x * y) • z = x • (y • z)
rw [mul_smul, ← h, f.apply_symm_apply] }
exact
ofRepr <|
(b.repr.restrictScalars R').trans <| Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm
