Mathlib v3 is deprecated. Go to Mathlib v4

Def mv_polynomial.monomial_one_hom

Modification history

2021-10-25 22:55

src/data/mv_polynomial/basic.lean

refactor(data/mv_polynomial): upgrade `monomial` to a `linear_map` (#9870)

Added mv_polynomial.monomial_one_hom View on Github →