Commit 2024-06-08 18:34 7e7e7b06

View on Github →

Chore(Algebra/Polynomial/Module/Basic): Refactor out Module.AEval (#13613) Refactor Module.AEval out of Algebra/Polynomial/Module/Basic.

Estimated changes

added theorem Module.AEval'_def
added theorem Module.AEval.C_smul
added theorem Module.AEval.X_smul_of
added def Module.AEval.of
added def Module.AEval
deleted def LinearMap.ofAEval
deleted theorem Module.AEval'.X_smul_of
deleted theorem Module.AEval'_def
deleted theorem Module.AEval.C_smul
deleted theorem Module.AEval.X_smul_of
deleted def Module.AEval.of
deleted theorem Module.AEval.of_symm_smul
deleted def Module.AEval