Theorem AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree

Modification history

2025-12-11 22:59

Mathlib/Algebra/MonoidAlgebra/Degree.lean

chore: use `Set.Nonempty` everywhere (#32697)

Modified AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree View on Github →

2024-09-09 01:17

Mathlib/Algebra/MonoidAlgebra/Degree.lean

feat: more API for AddMonoidAlgebra.supDegree / leadingCoeff / Monic (#7173) …

Added AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree View on Github →