mathlib3
42813431
- refactor(data/polynomial): redefine `C` as an `alg_hom` (#3003)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
refactor(data/polynomial): redefine `C` as an `alg_hom` (#3003) As a side effect Lean parses `C 1` as `polynomial nat`. If you need `polynomial R`, then use `C (1:R)`.
Author
urkud
Parents
34302c63
Loading