Zulip Chat Archive

Stream: general

Topic: polynomial.degree_map

Eric Rodriguez (Feb 02 2022 at 23:44):

there is a duplcation of lemmas (right below each other, actually). what name should they have instead?

Eric Rodriguez (Feb 02 2022 at 23:45):

/poll
degree_map_eq_of_injective
degree_map'

Eric Rodriguez (Feb 02 2022 at 23:46):

note that degree_map is taken by the special case for fields, which... probably should be generalized

Eric Rodriguez (Feb 03 2022 at 10:43):

#11792

Kevin Buzzard (Feb 05 2022 at 07:17):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC