English
If f: M ≃ₗ[R] N is an R-linear isomorphism compatible with a via hf, then AEval R M a ≃_{R[X]} N.
Русский
Если f: M ≃ₗ[R] N является тождественным по отношению к a через hf, то AEval R M a эквивалентно AEval R N a как R[X]-модули.
LaTeX
$$$\exists \; e : AEval\ R\ M\ a \simeq_{R[X]} N\;\text{с forward-мэпами как in LinearEquiv.ofAEval}$$$
Lean4
/-- Construct an `R[X]`-linear equivalence out of `AEval R M a` from a `R`-linear map out of `M`. -/
def _root_.LinearEquiv.ofAEval {N} [AddCommMonoid N] [Module R N] [Module R[X] N] [IsScalarTower R R[X] N]
(f : M ≃ₗ[R] N) (hf : ∀ m : M, f (a • m) = (X : R[X]) • f m) : AEval R M a ≃ₗ[R[X]] N
where
__ := LinearMap.ofAEval a f hf
invFun := (of R M a) ∘ f.symm
left_inv x := by simp [LinearMap.ofAEval]
right_inv x := by simp [LinearMap.ofAEval]
