Documentation Verification Report

FundamentalTheorem

📁 Source: Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

Statistics

Metric	Count
Definitions `accumulate`, `invAccumulate`, `esymmAlgEquiv`, `esymmAlgHom`, `esymmAlgHomMonomial`	5
Theorems `accumulate_apply`, `accumulate_injective`, `accumulate_invAccumulate`, `accumulate_last`, `accumulate_rec`, `antitone_supDegree`, `esymmAlgEquiv_apply`, `esymmAlgEquiv_symm_apply`, `esymmAlgHomMonomial_add`, `esymmAlgHomMonomial_single`, `esymmAlgHomMonomial_single_one`, `esymmAlgHom_apply`, `esymmAlgHom_fin_bijective`, `esymmAlgHom_fin_injective`, `esymmAlgHom_fin_surjective`, `esymmAlgHom_injective`, `esymmAlgHom_surjective`, `esymmAlgHom_zero`, `isSymmetric_esymmAlgHomMonomial`, `leadingCoeff_esymmAlgHomMonomial`, `monic_esymm`, `rename_esymmAlgHom`, `supDegree_esymm`, `supDegree_esymmAlgHomMonomial`	24
Total	29

Fin

Definitions

Name	Category	Theorems
`accumulate` 📖	CompOp	7 math math: `MvPolynomial.supDegree_esymmAlgHomMonomial`, `accumulate_invAccumulate`, `accumulate_rec`, `accumulate_apply`, `MvPolynomial.supDegree_esymm`, `accumulate_injective`, `accumulate_last`
`invAccumulate` 📖	CompOp	1 math math: `accumulate_invAccumulate`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accumulate_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `accumulate` `Finset.sum` `Nat.instAddCommMonoid` `Finset.filter` `Finset.univ` `fintype`	—	—
`accumulate_injective` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `accumulate`	—	`lt_or_ge` `add_right_cancel_iff` `AddRightCancelSemigroup.toIsRightCancelAdd` `LE.le.antisymm` `LE.le.trans` `LT.lt.nat_succ_le` `LT.lt.trans_eq` `accumulate_last` `LT.lt.not_ge` `LT.lt.trans_le`
`accumulate_invAccumulate` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `instPartialOrder` `Nat.instPreorder`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `accumulate` `invAccumulate`	—	`LT.lt.trans_le` `invAccumulate.eq_1` `LT.lt.trans_eq` `accumulate_last` `LE.le.not_gt` `Eq.not_gt`
`accumulate_last` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `accumulate` `LT.lt.trans_eq`	—	`LT.lt.trans_eq` `accumulate_apply` `Finset.sum_eq_single_of_mem` `Finset.mem_filter` `Finset.mem_univ` `le_rfl` `Eq.trans_le` `LT.lt.nat_succ_le` `LE.le.lt_of_ne` `Finset.mem_filter_univ`
`accumulate_rec` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `accumulate`	—	`Finset.sum_congr` `Finset.ext` `Finset.mem_erase` `Finset.add_sum_erase` `Finset.mem_filter` `Finset.mem_univ` `le_rfl`

MvPolynomial

Definitions

Name	Category	Theorems
`esymmAlgEquiv` 📖	CompOp	2 math math: `esymmAlgEquiv_apply`, `esymmAlgEquiv_symm_apply`
`esymmAlgHom` 📖	CompOp	8 math math: `rename_esymmAlgHom`, `esymmAlgHom_fin_surjective`, `esymmAlgHom_fin_injective`, `esymmAlgHom_apply`, `esymmAlgHom_fin_bijective`, `esymmAlgEquiv_apply`, `esymmAlgHom_surjective`, `esymmAlgHom_injective`
`esymmAlgHomMonomial` 📖	CompOp	7 math math: `isSymmetric_esymmAlgHomMonomial`, `supDegree_esymmAlgHomMonomial`, `esymmAlgHomMonomial_single`, `leadingCoeff_esymmAlgHomMonomial`, `esymmAlgHom_zero`, `esymmAlgHomMonomial_single_one`, `esymmAlgHomMonomial_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`esymmAlgEquiv_apply` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `AlgEquiv` `MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `esymmAlgEquiv` `AlgHom` `AlgHom.funLike` `esymmAlgHom`	—	—
`esymmAlgEquiv_symm_apply` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `AlgEquiv` `MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `esymmAlgEquiv` `esymm` `esymm_isSymmetric` `X`	—	`esymmAlgHom_injective` `Eq.ge` `esymm_isSymmetric` `AlgEquiv.ofBijective_apply_symm_apply` `aeval_X`
`esymmAlgHomMonomial_add` 📖	mathematical	—	`esymmAlgHomMonomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`esymmAlgHom_apply` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `monomial_mul` `mul_one`
`esymmAlgHomMonomial_single` 📖	mathematical	—	`esymmAlgHomMonomial` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `esymm`	—	`esymmAlgHomMonomial.eq_1` `esymmAlgHom_apply` `aeval_monomial` `algebraMap_eq` `Finsupp.prod_single_index` `pow_zero`
`esymmAlgHomMonomial_single_one` 📖	mathematical	—	`esymmAlgHomMonomial` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `commSemiring` `esymm`	—	`esymmAlgHomMonomial_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`esymmAlgHom_apply` 📖	mathematical	—	`MvPolynomial` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `esymmAlgHom` `aeval` `esymm`	—	`Subalgebra.mvPolynomial_aeval_coe`
`esymmAlgHom_fin_bijective` 📖	mathematical	—	`Function.Bijective` `MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `esymmAlgHom` `Fin.fintype`	—	`esymmAlgHom_fin_injective` `le_rfl` `AlgHom.mem_range` `eq_or_ne` `Subalgebra.zero_mem` `WellFoundedLT.induction` `Finsupp.Lex.wellFoundedLT` `instTrichotomousLt` `IsWellOrder.toIsWellFounded` `isWellOrder_gt` `Finite.to_wellFoundedGT` `Finite.of_fintype` `Nat.instCanonicallyOrderedAdd` `instWellFoundedLTNat` `DFunLike.ext'_iff` `supDegree_esymmAlgHomMonomial` `Zero.instNonempty` `AddMonoidAlgebra.leadingCoeff_eq_zero` `Equiv.injective` `Fin.accumulate_invAccumulate` `IsSymmetric.antitone_supDegree` `AlgHom.mem_range_self` `AddMonoidAlgebra.supDegree_sub_lt_of_leadingCoeff_eq` `leadingCoeff_esymmAlgHomMonomial` `Subalgebra.sub_mem` `isSymmetric_esymmAlgHomMonomial` `sub_add_cancel` `Subalgebra.add_mem` `sub_ne_zero`
`esymmAlgHom_fin_injective` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `esymmAlgHom` `Fin.fintype`	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Function.mtr` `as_sum` `map_sum` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Subalgebra.coe_eq_zero` `AddSubmonoidClass.coe_finset_sum` `AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree` `Nat.instCanonicallyOrderedAdd` `support_nonempty` `esymmAlgHomMonomial.eq_1` `Zero.instNonempty` `AddMonoidAlgebra.leadingCoeff_eq_zero` `Equiv.injective` `leadingCoeff_esymmAlgHomMonomial` `mem_support_iff` `DFunLike.ext'` `Fin.accumulate_injective` `supDegree_esymmAlgHomMonomial` `Finset.mem_coe` `DFunLike.ext'_iff`
`esymmAlgHom_fin_surjective` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `esymmAlgHom` `Fin.fintype`	—	`esymmAlgHom_fin_bijective` `AlgHom.mem_range` `induction_on` `algebraMap_eq` `AlgHom.commutes` `Subalgebra.algebraMap_mem` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Subalgebra.add_mem` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Subalgebra.mul_mem` `LT.lt.trans_le` `aeval_X`
`esymmAlgHom_injective` 📖	mathematical	`Fintype.card`	`MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `esymmAlgHom`	—	`rename_esymmAlgHom` `AlgHom.coe_comp` `AlgEquiv.injective` `esymmAlgHom_fin_injective`
`esymmAlgHom_surjective` 📖	mathematical	`Fintype.card`	`MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHom.funLike` `esymmAlgHom`	—	`rename_esymmAlgHom` `AlgHom.coe_comp` `AlgEquiv.surjective` `esymmAlgHom_fin_surjective`
`esymmAlgHom_zero` 📖	mathematical	—	`esymmAlgHomMonomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C`	—	`esymmAlgHomMonomial.eq_1` `monomial_zero'` `esymmAlgHom_apply` `aeval_C` `algebraMap_eq`
`isSymmetric_esymmAlgHomMonomial` 📖	mathematical	—	`IsSymmetric` `esymmAlgHomMonomial`	—	—
`leadingCoeff_esymmAlgHomMonomial` 📖	mathematical	—	`AddMonoidAlgebra.leadingCoeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Lex` `CommSemiring.toSemiring` `Finsupp.Lex.linearOrder` `Fin.instLinearOrder` `Nat.instLinearOrder` `Finsupp.Lex.orderBot` `Nat.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instCanonicallyOrderedAdd` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Finsupp.instInhabited` `esymmAlgHomMonomial` `Fin.fintype`	—	`Finsupp.induction₂` `Nat.instCanonicallyOrderedAdd` `esymmAlgHom_zero` `leadingCoeff_toLex_C` `esymmAlgHomMonomial_add` `esymmAlgHomMonomial_single_one` `Zero.instNonempty` `AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left` `Finsupp.Lex.addLeftStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.Lex.addRightStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `AddMonoidAlgebra.Monic.pow` `toLex_add` `Equiv.injective` `monic_esymm` `LT.lt.trans_le`
`monic_esymm` 📖	mathematical	—	`AddMonoidAlgebra.Monic` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Lex` `CommSemiring.toSemiring` `Finsupp.Lex.linearOrder` `Fin.instLinearOrder` `Nat.instLinearOrder` `Finsupp.Lex.orderBot` `Nat.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instCanonicallyOrderedAdd` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Finsupp.instInhabited` `esymm` `Fin.fintype`	—	`Nat.instCanonicallyOrderedAdd` `esymm_zero` `AddMonoidAlgebra.monic_one` `Equiv.injective` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim`
`rename_esymmAlgHom` 📖	mathematical	—	`AlgHom.comp` `MvPolynomial` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.toAlgHom` `renameSymmetricSubalgebra` `esymmAlgHom`	—	`algHom_ext` `aeval_X` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `rename_esymm`
`supDegree_esymm` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `AddMonoidAlgebra.supDegree` `CommSemiring.toSemiring` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finsupp.Lex.linearOrder` `Fin.instLinearOrder` `Nat.instLinearOrder` `Finsupp.Lex.orderBot` `Nat.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Nat.instCanonicallyOrderedAdd` `toLex` `esymm` `Fin.fintype` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `Fin.accumulate` `Finsupp.single`	—	`Nat.instCanonicallyOrderedAdd` `ofLex_toLex` `Finsupp.indicator_apply` `Finset.sum_congr` `Finsupp.single_apply` `Finset.sum_ite_eq`
`supDegree_esymmAlgHomMonomial` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `AddMonoidAlgebra.supDegree` `CommSemiring.toSemiring` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finsupp.Lex.linearOrder` `Fin.instLinearOrder` `Nat.instLinearOrder` `Finsupp.Lex.orderBot` `Nat.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Nat.instCanonicallyOrderedAdd` `toLex` `esymmAlgHomMonomial` `Fin.fintype` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `Fin.accumulate`	—	`Finsupp.induction₂` `Nat.instCanonicallyOrderedAdd` `esymmAlgHom_zero` `supDegree_toLex_C` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `LT.lt.trans_le` `esymmAlgHomMonomial_add` `esymmAlgHomMonomial_single_one` `AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left` `Finsupp.Lex.addLeftStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.Lex.addRightStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Equiv.injective` `toLex_add` `AddMonoidAlgebra.Monic.pow` `monic_esymm` `Zero.instNonempty` `AddMonoidAlgebra.leadingCoeff_eq_zero` `leadingCoeff_esymmAlgHomMonomial` `ofLex_add` `Finsupp.coe_add` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidAlgebra.Monic.supDegree_pow` `nontrivial_of_ne` `ofLex_smul` `Finsupp.coe_smul` `supDegree_esymm` `map_nsmul` `Finsupp.smul_single` `nsmul_one` `Nat.cast_id`

MvPolynomial.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_supDegree` 📖	mathematical	`MvPolynomial.IsSymmetric`	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instPreorder` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `AddMonoidAlgebra.supDegree` `CommSemiring.toSemiring` `Lattice.toSemilatticeSup` `Finsupp.Lex.linearOrder` `Nat.instLinearOrder` `Finsupp.Lex.orderBot` `Nat.instAddCommMonoid` `Nat.instCanonicallyOrderedAdd` `toLex`	—	`Nat.instCanonicallyOrderedAdd` `eq_or_ne` `AddMonoidAlgebra.supDegree_zero` `Finsupp.bot_eq_zero` `Pi.zero_mono` `Antitone.eq_1` `Mathlib.Tactic.Push.not_forall_eq` `LE.le.not_gt` `Finset.le_sup` `MvPolynomial.mem_support_iff` `MvPolynomial.coeff_rename_mapDomain` `Equiv.injective` `MvPolynomial.leadingCoeff_toLex` `Zero.instNonempty` `AddMonoidAlgebra.leadingCoeff_eq_zero` `Equiv.swap_apply_of_ne_of_ne` `LT.lt.ne` `LT.lt.trans_le` `Finsupp.mapDomain_apply` `AddMonoidAlgebra.supDegree.eq_1` `LT.lt.trans_eq` `Finsupp.mapDomain_equiv_apply` `Equiv.swap_apply_left`

---

← Back to Index