Variables

📁 Source: Mathlib/Algebra/MvPolynomial/Variables.lean

Statistics

Metric	Count
Definitions vars	1
Theorems aeval_eq_constantCoeff_of_vars, aeval_ite_mem_eq_self, eval₂Hom_congr', eval₂Hom_eq_constantCoeff_of_vars, exists_rename_eq_of_vars_subset_range, hom_congr_vars, leadingCoeff_toLex, leadingCoeff_toLex_C, mem_support_notMem_vars_zero, mem_vars, mem_vars_rename, supDegree_toLex_C, vars_0, vars_C, vars_C_mul, vars_X, vars_add_of_disjoint, vars_add_subset, vars_def, vars_eq_support_biUnion_support, vars_map, vars_map_of_injective, vars_monomial, vars_monomial_single, vars_mul, vars_one, vars_pow, vars_prod, vars_rename, vars_sum_of_disjoint, vars_sum_subset	31
Total	32

MvPolynomial

Definitions

Name	Category	Theorems
vars 📖	CompOp	43 math math: WittVector.remainder_vars, vars_X, mem_vars, wittStructureRat_vars, vars_monomial, vars_sub_subset, wittPolynomial_vars, WittVector.wittZSMul_vars, vars_eq_support_biUnion_support, mem_supported, wittPolynomial_vars_subset, vars_neg, WittVector.mul_polyOfInterest_vars, WittVector.wittAdd_vars, vars_C_mul, mem_supported_vars, vars_prod, wittStructureInt_vars, xInTermsOfW_vars_subset, vars_def, vars_map_of_injective, WittVector.wittSub_vars, WittVector.wittPow_vars, vars_one, vars_bind₁, vars_mul, vars_pow, vars_C, WittVector.polyOfInterest_vars, WittVector.polyOfInterest_vars_eq, vars_map, xInTermsOfW_vars_aux, vars_rename, WittVector.wittNSMul_vars, vars_add_subset, WittVector.wittNeg_vars, vars_sum_subset, WittVector.wittPolyProd_vars, supported_eq_vars_subset, vars_0, vars_monomial_single, WittVector.wittPolyProdRemainder_vars, WittVector.wittMul_vars

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_eq_constantCoeff_of_vars 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe AlgHom MvPolynomial commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom RingHom.instFunLike algebraMap constantCoeff	—	eval₂Hom_eq_constantCoeff_of_vars
aeval_ite_mem_eq_self 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike vars	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval Set.instMembership X MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	as_sum aeval_sum Finset.sum_congr aeval_monomial monomial_eq Finsupp.prod_congr mem_vars
eval₂Hom_congr' 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom	—	as_sum map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr eval₂Hom_monomial Finset.prod_congr mem_vars
eval₂Hom_eq_constantCoeff_of_vars 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe RingHom MvPolynomial commSemiring RingHom.instFunLike eval₂Hom constantCoeff	—	as_sum map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr eval₂Hom_monomial RingHom.map_zero Finset.sum_eq_zero Finset.nonempty_iff_ne_empty Finsupp.support_eq_empty Finsupp.notMem_support_iff coeff.eq_1 constantCoeff_eq Finsupp.prod.eq_1 Finset.prod_eq_zero mem_vars zero_pow Finsupp.mem_support_iff MulZeroClass.mul_zero Finset.sum_eq_single Finsupp.prod_zero_index mul_one
exists_rename_eq_of_vars_subset_range 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike vars Set.range	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	hom_congr_vars RingHom.ext algHom_C RingHomCompTriple.comp_eq RingHomCompTriple.right_ids aeval_X Function.partialInv_left rename_X
hom_congr_vars 📖	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	—	—	RingHom.congr_fun ringHom_ext' RingHom.ext eval₂_C eval₂Hom_X' eval₂Hom_congr'
leadingCoeff_toLex 📖	mathematical	—	AddMonoidAlgebra.leadingCoeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Lex CommSemiring.toSemiring Finsupp.Lex.linearOrder 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 coeff ofLex AddMonoidAlgebra.supDegree Lattice.toSemilatticeSup	—	Nat.instCanonicallyOrderedAdd AddMonoidAlgebra.leadingCoeff.eq_1 Equiv.injective Function.rightInverse_invFun Equiv.surjective toLex_ofLex
leadingCoeff_toLex_C 📖	mathematical	—	AddMonoidAlgebra.leadingCoeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Lex CommSemiring.toSemiring Finsupp.Lex.linearOrder 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 RingHom MvPolynomial Semiring.toNonAssocSemiring commSemiring RingHom.instFunLike C	—	AddMonoidAlgebra.leadingCoeff_single Nat.instCanonicallyOrderedAdd Equiv.injective
mem_support_notMem_vars_zero 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support vars	DFunLike.coe Finsupp.instFunLike	—	Mathlib.Tactic.Contrapose.contrapose₂ mem_vars Finsupp.mem_support_iff
mem_vars 📖	mathematical	—	Finset Finset.instMembership vars Finsupp MulZeroClass.toZero Nat.instMulZeroClass support Finsupp.support	—	vars_def
mem_vars_rename 📖	—	Finset Finset.instMembership vars DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename	—	—	vars_rename
supDegree_toLex_C 📖	mathematical	—	AddMonoidAlgebra.supDegree Finsupp MulZeroClass.toZero Nat.instMulZeroClass Lex CommSemiring.toSemiring Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Finsupp.Lex.linearOrder Nat.instLinearOrder Finsupp.Lex.orderBot Nat.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Nat.instCanonicallyOrderedAdd DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toLex RingHom MvPolynomial Semiring.toNonAssocSemiring commSemiring RingHom.instFunLike C instZeroLex Finsupp.instZero	—	Nat.instCanonicallyOrderedAdd AddMonoidAlgebra.supDegree_single ite_eq_iff'
vars_0 📖	mathematical	—	vars MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset Finset.instEmptyCollection	—	vars_def degrees_zero Multiset.toFinset_zero
vars_C 📖	mathematical	—	vars DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Finset Finset.instEmptyCollection	—	vars_def degrees_C Multiset.toFinset_zero
vars_C_mul 📖	mathematical	—	vars CommRing.toCommSemiring MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C	—	Finset.ext coeff_C_mul mul_ne_zero_iff
vars_X 📖	mathematical	—	vars X Finset Finset.instSingleton	—	X.eq_1 vars_monomial one_ne_zero' NeZero.one Finsupp.support_single_ne_zero
vars_add_of_disjoint 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot vars	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.instUnion	—	HasSubset.Subset.antisymm Finset.instAntisymmSubset vars_add_subset vars_def degrees_add_of_disjoint Multiset.toFinset_union
vars_add_subset 📖	mathematical	—	Finset Finset.instHasSubset vars MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.instUnion	—	vars_def Multiset.mem_of_le degrees_add_le
vars_def 📖	mathematical	—	vars Multiset.toFinset degrees	—	vars.eq_1 Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable
vars_eq_support_biUnion_support 📖	mathematical	—	vars Finset.biUnion Finsupp MulZeroClass.toZero Nat.instMulZeroClass support Finsupp.support	—	Finset.ext mem_vars Finset.mem_biUnion
vars_map 📖	mathematical	—	Finset Finset.instHasSubset vars DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map	—	vars_def Multiset.subset_of_le degrees_map_le
vars_map_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	vars MvPolynomial commSemiring map	—	degrees_map_of_injective
vars_monomial 📖	mathematical	—	vars DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass	—	vars_def degrees_monomial_eq Finsupp.toFinset_toMultiset
vars_monomial_single 📖	mathematical	—	vars DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instSingleton	—	vars_monomial Finsupp.support_single_ne_zero
vars_mul 📖	mathematical	—	Finset Finset.instHasSubset vars MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.instUnion	—	vars_def Multiset.subset_of_le degrees_mul_le
vars_one 📖	mathematical	—	vars MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset Finset.instEmptyCollection	—	vars_C
vars_pow 📖	mathematical	—	Finset Finset.instHasSubset vars MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring	—	pow_zero vars_one pow_succ' Finset.Subset.trans vars_mul Finset.union_subset Finset.Subset.refl
vars_prod 📖	mathematical	—	Finset Finset.instHasSubset vars Finset.prod MvPolynomial CommSemiring.toCommMonoid commSemiring Finset.biUnion	—	Finset.induction_on vars_one Finset.instReflSubset Finset.prod_insert Finset.biUnion_insert Finset.Subset.trans vars_mul Finset.union_subset_union Finset.Subset.refl
vars_rename 📖	mathematical	—	Finset Finset.instHasSubset vars DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike rename Finset.image	—	vars_def degrees_rename
vars_sum_of_disjoint 📖	mathematical	Pairwise Function.onFun Finset Disjoint Finset.partialOrder Finset.instOrderBot vars	Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.biUnion	—	Finset.induction_on vars_0 Finset.biUnion_insert Finset.sum_insert vars_add_of_disjoint
vars_sum_subset 📖	mathematical	—	Finset Finset.instHasSubset vars Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.biUnion	—	Finset.induction_on vars_0 Finset.instReflSubset Finset.biUnion_insert Finset.sum_insert Finset.Subset.trans vars_add_subset Finset.union_subset_union Finset.Subset.refl

---

← Back to Index