Defs

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

Statistics

Metric	Count
Definitions `esymm`, `IsSymmetric`, `esymm`, `esymmPart`, `hsymm`, `hsymmPart`, `msymm`, `psum`, `psumPart`, `renameSymmetricSubalgebra`, `symmetricSubalgebra`	11
Theorems `esymm_map_val`, `esymm_pair_one`, `esymm_pair_two`, `pow_smul_esymm`, `C`, `add`, `map`, `mul`, `neg`, `one`, `rename`, `smul`, `sub`, `zero`, `aeval_esymm_eq_multiset_esymm`, `degrees_esymm`, `esymmPart_indiscrete`, `esymmPart_zero`, `esymm_eq_multiset_esymm`, `esymm_eq_sum_monomial`, `esymm_eq_sum_subtype`, `esymm_isSymmetric`, `esymm_one`, `esymm_zero`, `hsymmPart_indiscrete`, `hsymmPart_zero`, `hsymm_isSymmetric`, `hsymm_one`, `hsymm_zero`, `isSymmetric_rename`, `map_esymm`, `map_hsymm`, `mem_symmetricSubalgebra`, `msymm_isSymmetric`, `msymm_one`, `msymm_zero`, `psumPart_indiscrete`, `psumPart_zero`, `psum_isSymmetric`, `psum_one`, `psum_zero`, `renameSymmetricSubalgebra_apply_coe`, `renameSymmetricSubalgebra_symm_apply_coe`, `rename_esymm`, `rename_hsymm`, `rename_msymm`, `rename_psum`, `support_esymm`, `support_esymm'`, `support_esymm''`	50
Total	61

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`esymm_map_val` 📖	mathematical	—	`Multiset.esymm` `Multiset.map` `val` `sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `powersetCard` `prod` `CommSemiring.toCommMonoid`	—	`Multiset.map_congr` `Multiset.powersetCard_map` `Multiset.map_map`

Multiset

Definitions

Name	Category	Theorems
`esymm` 📖	CompOp	14 math math: `prod_X_sub_X_eq_sum_esymm`, `prod_X_add_C_coeff`, `MvPolynomial.aeval_esymm_eq_multiset_esymm`, `esymm_neg`, `pow_smul_esymm`, `Finset.esymm_map_val`, `MvPolynomial.esymm_eq_multiset_esymm`, `Polynomial.coeff_eq_esymm_roots_of_card`, `Polynomial.coeff_eq_esymm_roots_of_splits`, `esymm_pair_two`, `prod_X_add_C_eq_sum_esymm`, `prod_X_add_C_coeff'`, `esymm_pair_one`, `prod_X_sub_C_coeff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`esymm_pair_one` 📖	mathematical	—	`esymm` `cons` `Multiset` `instSingleton` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`map_congr` `powersetCard_cons` `zero_add` `powersetCard_one` `powersetCard_zero_left` `add_comm` `map_cons` `prod_singleton` `sum_cons` `sum_singleton`
`esymm_pair_two` 📖	mathematical	—	`esymm` `cons` `Multiset` `instSingleton` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`map_congr` `powersetCard_cons` `powersetCard_eq_empty` `card_singleton` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `powersetCard_one` `zero_add` `prod_cons` `prod_singleton` `sum_singleton`
`pow_smul_esymm` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Monoid.toNatPow` `esymm` `map`	—	`esymm.eq_1` `smul_sum` `map_map` `map_congr` `mem_powersetCard` `smul_prod` `powersetCard_map`

MvPolynomial

Definitions

Name	Category	Theorems
`IsSymmetric` 📖	MathDef	10 math math: `esymm_isSymmetric`, `isSymmetric_esymmAlgHomMonomial`, `IsSymmetric.one`, `psum_isSymmetric`, `IsSymmetric.zero`, `msymm_isSymmetric`, `IsSymmetric.C`, `isSymmetric_rename`, `mem_symmetricSubalgebra`, `hsymm_isSymmetric`
`esymm` 📖	CompOp	25 math math: `esymm_isSymmetric`, `sum_antidiagonal_card_esymm_psum_eq_zero`, `esymmAlgHomMonomial_single`, `map_esymm`, `rename_esymm`, `supDegree_esymm`, `support_esymm'`, `mul_esymm_eq_sum`, `monic_esymm`, `prod_X_add_C_coeff`, `esymmAlgHomMonomial_single_one`, `aeval_esymm_eq_multiset_esymm`, `prod_C_add_X_eq_sum_esymm`, `esymmAlgHom_apply`, `degrees_esymm`, `esymm_eq_sum_monomial`, `psum_eq_mul_esymm_sub_sum`, `esymm_eq_multiset_esymm`, `support_esymm''`, `esymm_zero`, `esymm_eq_sum_subtype`, `esymm_one`, `support_esymm`, `esymmPart_indiscrete`, `esymmAlgEquiv_symm_apply`
`esymmPart` 📖	CompOp	2 math math: `esymmPart_zero`, `esymmPart_indiscrete`
`hsymm` 📖	CompOp	6 math math: `hsymmPart_indiscrete`, `map_hsymm`, `hsymm_one`, `hsymm_zero`, `rename_hsymm`, `hsymm_isSymmetric`
`hsymmPart` 📖	CompOp	2 math math: `hsymmPart_indiscrete`, `hsymmPart_zero`
`msymm` 📖	CompOp	4 math math: `rename_msymm`, `msymm_zero`, `msymm_isSymmetric`, `msymm_one`
`psum` 📖	CompOp	8 math math: `sum_antidiagonal_card_esymm_psum_eq_zero`, `rename_psum`, `psum_isSymmetric`, `psumPart_indiscrete`, `psum_zero`, `mul_esymm_eq_sum`, `psum_one`, `psum_eq_mul_esymm_sub_sum`
`psumPart` 📖	CompOp	2 math math: `psumPart_indiscrete`, `psumPart_zero`
`renameSymmetricSubalgebra` 📖	CompOp	3 math math: `rename_esymmAlgHom`, `renameSymmetricSubalgebra_symm_apply_coe`, `renameSymmetricSubalgebra_apply_coe`
`symmetricSubalgebra` 📖	CompOp	12 math math: `rename_esymmAlgHom`, `esymmAlgHom_fin_surjective`, `renameSymmetricSubalgebra_symm_apply_coe`, `esymmAlgHom_fin_injective`, `esymmAlgHom_apply`, `mem_symmetricSubalgebra`, `esymmAlgHom_fin_bijective`, `esymmAlgEquiv_apply`, `esymmAlgHom_surjective`, `esymmAlgEquiv_symm_apply`, `esymmAlgHom_injective`, `renameSymmetricSubalgebra_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_esymm_eq_multiset_esymm` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `esymm` `Multiset.esymm` `Multiset.map` `Finset.val` `Finset.univ`	—	`aeval_sum` `Finset.sum_congr` `aeval_prod` `Finset.prod_congr` `aeval_X` `Finset.esymm_map_val`
`degrees_esymm` 📖	mathematical	`Fintype.card`	`degrees` `esymm` `Finset.val` `Finset.univ`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_congr` `Finsupp.toMultiset_single` `one_smul` `Finset.sum_multiset_singleton` `degrees_def` `support_esymm` `Finset.sup_image` `Finset.comp_sup_eq_sup_comp` `Finset.union_val` `LT.lt.ne'` `Finset.powersetCard_sup`
`esymmPart_indiscrete` 📖	mathematical	—	`esymmPart` `Nat.Partition.indiscrete` `esymm`	—	`Multiset.map_congr` `Nat.Partition.partition_zero_parts` `esymm_zero` `Nat.Partition.indiscrete_parts` `Multiset.prod_singleton`
`esymmPart_zero` 📖	mathematical	—	`esymmPart` `Nat.Partition.indiscrete` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Multiset.map_congr` `Nat.Partition.partition_zero_parts`
`esymm_eq_multiset_esymm` 📖	mathematical	—	`esymm` `Multiset.esymm` `MvPolynomial` `commSemiring` `Multiset.map` `X` `Finset.val` `Finset.univ`	—	`Finset.esymm_map_val`
`esymm_eq_sum_monomial` 📖	mathematical	—	`esymm` `Finset.sum` `Finset` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.powersetCard` `Finset.univ` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_congr` `monomial_sum_one` `Finset.prod_congr` `pow_one`
`esymm_eq_sum_subtype` 📖	mathematical	—	`esymm` `Finset.sum` `Finset` `Finset.card` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.univ` `Subtype.fintype` `Finset.fintype` `Finset.prod` `CommSemiring.toCommMonoid` `X`	—	`Finset.sum_subtype` `Finset.mem_powersetCard_univ`
`esymm_isSymmetric` 📖	mathematical	—	`IsSymmetric` `esymm`	—	`rename_esymm`
`esymm_one` 📖	mathematical	—	`esymm` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.univ` `X`	—	`Finset.singleton_injective` `Finset.sum_congr` `Finset.powersetCard_one` `Finset.sum_map` `Finset.prod_singleton`
`esymm_zero` 📖	mathematical	—	`esymm` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Finset.sum_congr` `Finset.powersetCard_zero` `Finset.sum_singleton`
`hsymmPart_indiscrete` 📖	mathematical	—	`hsymmPart` `Nat.Partition.indiscrete` `hsymm`	—	`Multiset.map_congr` `Nat.Partition.partition_zero_parts` `hsymm_zero` `Nat.Partition.indiscrete_parts` `Multiset.prod_singleton`
`hsymmPart_zero` 📖	mathematical	—	`hsymmPart` `Nat.Partition.indiscrete` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Multiset.map_congr` `Nat.Partition.partition_zero_parts`
`hsymm_isSymmetric` 📖	mathematical	—	`IsSymmetric` `hsymm`	—	`rename_hsymm`
`hsymm_one` 📖	mathematical	—	`hsymm` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.univ` `X`	—	`Fintype.sum_equiv` `Multiset.prod_singleton`
`hsymm_zero` 📖	mathematical	—	`hsymm` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Finset.sum_congr` `Finset.univ_unique` `Sym.eq_nil_of_card_zero` `Multiset.map_congr` `Finset.sum_const` `Finset.card_singleton` `one_smul`
`isSymmetric_rename` 📖	mathematical	—	`IsSymmetric` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`rename_rename` `Equiv.symm_comp_self` `rename_id` `IsSymmetric.rename`
`map_esymm` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `map` `esymm`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finset.prod_congr` `map_X`
`map_hsymm` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `map` `hsymm`	—	`Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Multiset.map_congr` `map_X`
`mem_symmetricSubalgebra` 📖	mathematical	—	`MvPolynomial` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `IsSymmetric`	—	—
`msymm_isSymmetric` 📖	mathematical	—	`IsSymmetric` `msymm`	—	`rename_msymm`
`msymm_one` 📖	mathematical	—	`msymm` `Nat.Partition.indiscrete` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.univ` `X`	—	`Nat.Partition.ofSym_one` `Fintype.sum_equiv` `Multiset.prod_singleton` `Multiset.map_singleton`
`msymm_zero` 📖	mathematical	—	`msymm` `Nat.Partition.indiscrete` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`msymm.eq_1` `Fintype.sum_subsingleton` `instSubsingletonSubtype_mathlib` `Unique.instSubsingleton`
`psumPart_indiscrete` 📖	mathematical	—	`psumPart` `Nat.Partition.indiscrete` `psum`	—	`Multiset.map_congr` `Nat.Partition.indiscrete_parts` `Multiset.prod_singleton`
`psumPart_zero` 📖	mathematical	—	`psumPart` `Nat.Partition.indiscrete` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Multiset.map_congr` `Nat.Partition.partition_zero_parts`
`psum_isSymmetric` 📖	mathematical	—	`IsSymmetric` `psum`	—	`rename_psum`
`psum_one` 📖	mathematical	—	`psum` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.univ` `X`	—	`Finset.sum_congr` `pow_one`
`psum_zero` 📖	mathematical	—	`psum` `MvPolynomial` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Fintype.card`	—	`Finset.sum_congr` `pow_zero` `Finset.sum_const` `nsmul_eq_mul` `mul_one`
`renameSymmetricSubalgebra_apply_coe` 📖	mathematical	—	`MvPolynomial` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgEquiv` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `renameSymmetricSubalgebra` `AlgHom` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`renameSymmetricSubalgebra_symm_apply_coe` 📖	mathematical	—	`MvPolynomial` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `symmetricSubalgebra` `DFunLike.coe` `AlgEquiv` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `renameSymmetricSubalgebra` `AlgHom` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`rename_esymm` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `esymm`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Finset.prod_congr` `rename_X` `Finset.powersetCard_map` `Finset.sum_map` `Finset.mapEmbedding_apply` `Finset.prod_map` `Finset.map_univ_equiv`
`rename_hsymm` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `hsymm`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Multiset.map_congr` `rename_X` `Fintype.sum_equiv` `Multiset.map_map`
`rename_msymm` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `msymm`	—	`msymm.eq_1` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Fintype.sum_equiv` `Multiset.prod_hom` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Multiset.map_map` `Nat.Partition.ofSymShapeEquiv.eq_1` `Multiset.map_congr` `rename_X`
`rename_psum` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `psum`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `rename_X` `Equiv.sum_comp`
`support_esymm` 📖	mathematical	—	`support` `esymm` `Finset.image` `Finset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instDecidableEq` `Finset.sum` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Finsupp.single` `Finset.powersetCard` `Finset.univ`	—	`support_esymm'` `Finset.biUnion_singleton`
`support_esymm'` 📖	mathematical	—	`support` `esymm` `Finset.biUnion` `Finset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instDecidableEq` `Finset.powersetCard` `Finset.univ` `Finset.instSingleton` `Finset.sum` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Finsupp.single`	—	`support_esymm''` `Finsupp.support_single_ne_zero` `one_ne_zero` `NeZero.one`
`support_esymm''` 📖	mathematical	—	`support` `esymm` `Finset.biUnion` `Finset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instDecidableEq` `Finset.powersetCard` `Finset.univ` `Finsupp.support` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.single` `Finset.sum` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`esymm_eq_sum_monomial` `Finset.sum_congr` `Finsupp.support_sum_eq_biUnion` `Finset.disjoint_left` `Finsupp.support_single_ne_zero` `one_ne_zero` `NeZero.one` `Finset.biUnion_congr` `Finset.biUnion_singleton_eq_self`

MvPolynomial.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C` 📖	mathematical	—	`MvPolynomial.IsSymmetric` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C`	—	`Subalgebra.algebraMap_mem`
`add` 📖	mathematical	`MvPolynomial.IsSymmetric`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Subalgebra.add_mem`
`map` 📖	mathematical	`MvPolynomial.IsSymmetric`	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map`	—	`MvPolynomial.map_rename`
`mul` 📖	mathematical	`MvPolynomial.IsSymmetric`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Subalgebra.mul_mem`
`neg` 📖	mathematical	`MvPolynomial.IsSymmetric` `CommRing.toCommSemiring`	`MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`Subalgebra.neg_mem`
`one` 📖	mathematical	—	`MvPolynomial.IsSymmetric` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Subalgebra.one_mem`
`rename` 📖	mathematical	`MvPolynomial.IsSymmetric`	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.rename` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`MvPolynomial.rename_injective` `Equiv.injective` `MvPolynomial.rename_rename` `Equiv.self_trans_symm` `MvPolynomial.rename_id_apply`
`smul` 📖	mathematical	`MvPolynomial.IsSymmetric`	`MvPolynomial` `Algebra.toSMul` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id`	—	`Subalgebra.smul_mem`
`sub` 📖	mathematical	`MvPolynomial.IsSymmetric` `CommRing.toCommSemiring`	`MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`Subalgebra.sub_mem`
`zero` 📖	mathematical	—	`MvPolynomial.IsSymmetric` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Subalgebra.zero_mem`

---

← Back to Index