Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 07:10 b6041198

View on Github →

feat(data/polynomial): Polynomial modules (#15065)

Estimated changes

Created src/data/polynomial/module.lean

added def polynomial_module.equiv_polynomial

added def polynomial_module.equiv_polynomial_self

added theorem polynomial_module.induction_linear

added def polynomial_module.lsingle

added theorem polynomial_module.lsingle_apply

added theorem polynomial_module.monomial_smul_apply

added theorem polynomial_module.monomial_smul_single

added def polynomial_module.single

added theorem polynomial_module.single_apply

added theorem polynomial_module.single_smul

added theorem polynomial_module.smul_apply

added theorem polynomial_module.smul_single_apply

added def polynomial_module

Modified src/ring_theory/finiteness.lean

added theorem module_polynomial_of_endo_smul_def