homogeneous): refactor using weighted_homogeneous
#17856

Open

feat(ring_theory/mv_polynomial/homogeneous): refactor using weighted_homogeneous #17856

mariainesdff wants to merge 7 commits into master from mariainesdff/homogeneous

add weighted_homogeneous.lean

99438650

move to ring_theory

386c08c8

add le_weighted_total_degree lemma

cb298e71

feat(ring_theory/mv_polynomial/weighted_homogeneous): add weighted ho…

1e663517

progress on homogeneous.lean

7eb9cbf7

partial proof

63ff55ea

finish homogeneous.lean

59a4fe05

mariainesdff added awaiting-review

mathlib-dependent-issues-bot added blocked-by-other-PR

mathlib-dependent-issues-bot removed blocked-by-other-PR

kbuzzard commented on 2023-05-09

kbuzzard removed awaiting-review

kbuzzard added awaiting-author

kim-em added too-late

Reviewers

kbuzzard

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone