English
PowerBasis.map pb e constructs the power basis for S' generated by e(pb.gen) from a power basis pb of S via an algebra isomorphism e: S ≃ₐ[R] S'.
Русский
PowerBasis.map pb e строит базис по степеням для S', порожденный e(pb.gen) из базиса pb для S через алгебраическое изоморфизм e: S ≃ₐ[R] S'.
LaTeX
$$$ \text{PowerBasis.map}(pb,e) : \text{PowerBasis } R S' $$$
Lean4
/-- `PowerBasis.map pb (e : S ≃ₐ[R] S')` is the power basis for `S'` generated by `e pb.gen`. -/
@[simps dim gen basis]
noncomputable def map (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : PowerBasis R S'
where
dim := pb.dim
basis := pb.basis.map e.toLinearEquiv
gen := e pb.gen
basis_eq_pow i := by rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]
