Commit 2023-04-21 15:12 a1e24bee

View on Github →

feat: port Data.Polynomial.Module (#3407)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Module.lean

added theorem PolynomialModule.add_apply

added theorem PolynomialModule.comp_eval

added theorem PolynomialModule.comp_single

added theorem PolynomialModule.comp_smul

added def PolynomialModule.eval

added theorem PolynomialModule.eval_lsingle

added theorem PolynomialModule.eval_map'

added theorem PolynomialModule.eval_map

added theorem PolynomialModule.eval_single

added theorem PolynomialModule.eval_smul

added theorem PolynomialModule.induction_linear

added theorem PolynomialModule.lsingle_apply

added theorem PolynomialModule.map_single

added theorem PolynomialModule.map_smul

added theorem PolynomialModule.monomial_smul_apply

added theorem PolynomialModule.monomial_smul_single

added theorem PolynomialModule.single_apply

added theorem PolynomialModule.single_smul

added theorem PolynomialModule.smul_apply

added theorem PolynomialModule.smul_single_apply

added theorem PolynomialModule.zero_apply

added def PolynomialModule