Commit 2024-11-23 14:14 d6a85bb4
View on Github →feat(Polynomial): p.natDegree = q.natDegree
if p.degree = q.degree
(#19402)
Also generalise natDegree_lt_natDegree
to two rings
From GrowthInGroups (LeanCamCombi)
feat(Polynomial): p.natDegree = q.natDegree
if p.degree = q.degree
(#19402)
Also generalise natDegree_lt_natDegree
to two rings
From GrowthInGroups (LeanCamCombi)