Supported

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

Statistics

Metric	Count
Definitions supported, supportedEquivMvPolynomial	2
Theorems X_mem_supported, exists_restrict_to_vars, mem_supported, mem_supported_vars, supportedEquivMvPolynomial_symm_C, supportedEquivMvPolynomial_symm_X, supported_empty, supported_eq_adjoin_X, supported_eq_range_rename, supported_eq_vars_subset, supported_le_supported_iff, supported_mono, supported_strictMono, supported_univ	14
Total	16

MvPolynomial

Definitions

Name	Category	Theorems
supported 📖	CompOp	17 math math: supportedEquivMvPolynomial_symm_X, supported_eq_adjoin_X, transcendental_supported_X_iff, mem_supported, supported_strictMono, supported_mono, mem_supported_vars, X_mem_supported, supported_le_supported_iff, supported_empty, supported_univ, transcendental_supported_polynomial_aeval_X_iff, supportedEquivMvPolynomial_symm_C, supported_eq_range_rename, transcendental_supported_X, supported_eq_vars_subset, transcendental_supported_polynomial_aeval_X
supportedEquivMvPolynomial 📖	CompOp	2 math math: supportedEquivMvPolynomial_symm_X, supportedEquivMvPolynomial_symm_C

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_mem_supported 📖	mathematical	—	MvPolynomial Subalgebra CommSemiring.toSemiring commSemiring algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported X Set Set.instMembership	—	vars_X Finset.coe_singleton
exists_restrict_to_vars 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike vars Int.instCommSemiring	Set.Elem Set.instMembership DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring CommRing.toCommSemiring algebra Algebra.id Ring.toIntAlgebra CommRing.toRing AlgHom.funLike aeval	—	AlgHom.mem_range supported_eq_range_rename mem_supported aeval_rename
mem_supported 📖	mathematical	—	MvPolynomial Subalgebra CommSemiring.toSemiring commSemiring algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike vars	—	supported_eq_range_rename AlgHom.mem_range trans Set.instIsTransSubset Finset.coe_subset vars_rename Finset.coe_image Subtype.coe_preimage_self exists_rename_eq_of_vars_subset_range Subtype.val_injective Subtype.range_coe_subtype
mem_supported_vars 📖	mathematical	—	MvPolynomial Subalgebra CommSemiring.toSemiring commSemiring algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported SetLike.coe Finset Finset.instSetLike vars	—	mem_supported subset_refl Set.instReflSubset
supportedEquivMvPolynomial_symm_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Set.Elem Subalgebra CommSemiring.toSemiring commSemiring algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported Subalgebra.toSemiring Subalgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm supportedEquivMvPolynomial RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C algebraMap	—	supported_eq_range_rename algHom_C
supportedEquivMvPolynomial_symm_X 📖	mathematical	—	MvPolynomial Subalgebra CommSemiring.toSemiring commSemiring algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported DFunLike.coe AlgEquiv Set.Elem Subalgebra.toSemiring Subalgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm supportedEquivMvPolynomial X Set Set.instMembership	—	supported_eq_range_rename rename_X
supported_empty 📖	mathematical	—	supported Set Set.instEmptyCollection Bot.bot Subalgebra MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Set.image_empty Algebra.adjoin_empty
supported_eq_adjoin_X 📖	mathematical	—	supported Algebra.adjoin MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id Set.image X	—	—
supported_eq_range_rename 📖	mathematical	—	supported AlgHom.range MvPolynomial Set Set.instMembership CommSemiring.toSemiring commSemiring algebra Algebra.id rename	—	supported.eq_1 Set.image_eq_range Algebra.adjoin_range_eq_range_aeval rename.eq_1
supported_eq_vars_subset 📖	mathematical	—	SetLike.coe Subalgebra MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id Subalgebra.instSetLike supported setOf Set Set.instHasSubset Finset Finset.instSetLike vars	—	Set.ext mem_supported
supported_le_supported_iff 📖	mathematical	—	Subalgebra MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder supported Set Set.instHasSubset	—	supported_mono
supported_mono 📖	mathematical	Set Set.instHasSubset	Subalgebra MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder supported	—	Algebra.adjoin_mono Set.image_mono
supported_strictMono 📖	mathematical	—	StrictMono Set Subalgebra MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Subalgebra.instPartialOrder supported	—	strictMono_of_le_iff_le supported_le_supported_iff
supported_univ 📖	mathematical	—	supported Set.univ Top.top Subalgebra MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

---

← Back to Index