Commit 2024-09-09 01:17 dbed408f

View on Github →

feat: more API for AddMonoidAlgebra.supDegree / leadingCoeff / Monic (#7173) Infrastructure for working with monomial orders on MvPolynomial rings. The lexicographic order is used in #6593 (proof of the fundamental theorem of symmetric polynomials)

Estimated changes

Modified Mathlib/Algebra/Group/Subsemigroup/Basic.lean

modified theorem Subsemigroup.coe_set_mk

Modified Mathlib/Algebra/Group/Subsemigroup/Operations.lean

added theorem MulHom.srange_mk

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

added theorem AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left

added theorem AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right

added theorem AddMonoidAlgebra.Monic.mul

added theorem AddMonoidAlgebra.Monic.ne_zero

added theorem AddMonoidAlgebra.Monic.pow

added theorem AddMonoidAlgebra.Monic.supDegree_mul

added theorem AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left

added theorem AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right

added theorem AddMonoidAlgebra.Monic.supDegree_pow

added def AddMonoidAlgebra.Monic

added theorem AddMonoidAlgebra.apply_supDegree_add_supDegree

added theorem AddMonoidAlgebra.exists_supDegree_mem_support

added theorem AddMonoidAlgebra.leadingCoeff_add_eq_left

added theorem AddMonoidAlgebra.leadingCoeff_add_eq_right

added theorem AddMonoidAlgebra.leadingCoeff_eq_zero

added theorem AddMonoidAlgebra.leadingCoeff_mul

added theorem AddMonoidAlgebra.leadingCoeff_single

added theorem AddMonoidAlgebra.leadingCoeff_zero

added theorem AddMonoidAlgebra.monic_one

added theorem AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree'

added theorem AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree

added theorem AddMonoidAlgebra.supDegree_add_eq_left

added theorem AddMonoidAlgebra.supDegree_add_eq_right

added theorem AddMonoidAlgebra.supDegree_eq_of_isMaxOn

added theorem AddMonoidAlgebra.supDegree_eq_of_max

added theorem AddMonoidAlgebra.supDegree_leadingCoeff_sum_eq

added theorem AddMonoidAlgebra.supDegree_mem_range

added theorem AddMonoidAlgebra.supDegree_mem_support

added theorem AddMonoidAlgebra.supDegree_mul

added theorem AddMonoidAlgebra.supDegree_sub_lt_of_leadingCoeff_eq

added theorem AddMonoidAlgebra.supDegree_sum_lt

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

added theorem MvPolynomial.leadingCoeff_toLex

added theorem MvPolynomial.leadingCoeff_toLex_C

added theorem MvPolynomial.supDegree_toLex_C

Modified Mathlib/Order/Filter/Extr.lean

added theorem inf_eq_of_isMinOn

added theorem inf_eq_of_min

added theorem sup_eq_of_isMaxOn

added theorem sup_eq_of_max