Commit 2023-06-08 18:15 5d808684

View on Github →

feat: port RingTheory.WittVector.IsPoly (#4851) This file contains a couple of tactics. I ported everything that is not a tactic and added an "attributes" file. My plan is to try to develop the tactics while porting a file that actually uses them.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/IsPoly.lean

added theorem WittVector.IsPoly.comp

added theorem WittVector.IsPoly.comp₂

added theorem WittVector.IsPoly.ext

added theorem WittVector.IsPoly.map

added theorem WittVector.IsPoly₂.comp

added theorem WittVector.IsPoly₂.compLeft

added theorem WittVector.IsPoly₂.compRight

added theorem WittVector.IsPoly₂.diag

added theorem WittVector.IsPoly₂.ext

added theorem WittVector.IsPoly₂.map

added theorem WittVector.addIsPoly₂

added theorem WittVector.bind₁_onePoly_wittPolynomial

added theorem WittVector.bind₁_zero_wittPolynomial

added theorem WittVector.mulIsPoly₂

added theorem WittVector.negIsPoly

added def WittVector.onePoly

added theorem WittVector.poly_eq_of_wittPolynomial_bind_eq'

added theorem WittVector.poly_eq_of_wittPolynomial_bind_eq

Created Mathlib/RingTheory/WittVector/WittAttributes.lean