Expand

📁 Source: Mathlib/RingTheory/MvPowerSeries/Expand.lean

Statistics

Metric	Count
Definitions `expand`	1
Theorems `expand`, `coeff_expand_of_not_dvd`, `coeff_expand_smul`, `constantCoeff_expand`, `expand_C`, `expand_X`, `expand_comp_substAlgHom`, `expand_eq_expand`, `expand_monomial`, `expand_mul`, `expand_mul_eq_comp`, `expand_one`, `expand_one_apply`, `expand_subst`, `expand_substAlgHom`, `map_expand`, `map_frobenius_expand`, `map_iterateFrobenius_expand`, `order_expand`, `support_expand`, `support_expand_subset`, `trunc'_expand`, `trunc'_expand_trunc'`	23
Total	24

MvPowerSeries

Definitions

Name	Category	Theorems
`expand` 📖	CompOp	23 math math: `support_expand`, `PowerSeries.expand_subst`, `expand_mul`, `expand_substAlgHom`, `expand_one_apply`, `expand_eq_expand`, `expand_one`, `coeff_expand_smul`, `trunc'_expand`, `expand_subst`, `expand_comp_substAlgHom`, `expand_monomial`, `order_expand`, `map_iterateFrobenius_expand`, `coeff_expand_of_not_dvd`, `map_frobenius_expand`, `expand_X`, `map_expand`, `constantCoeff_expand`, `support_expand_subset`, `expand_mul_eq_comp`, `HasSubst.expand`, `expand_C`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_expand_of_not_dvd` 📖	mathematical	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	`LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `finsum_eq_zero_of_forall_eq_zero` `MulZeroClass.mul_zero` `substAlgHom_apply` `HasSubst.X_pow` `coeff_subst` `monomial_smul_eq` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `coeff_monomial`
`coeff_expand_smul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instNatSMul` `Nat.instAddMonoid` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`substAlgHom_apply` `HasSubst.X_pow` `coeff_subst` `monomial_smul_eq` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `finsum_eq_single` `coeff_monomial` `Finsupp.instIsAddTorsionFree` `Nat.instIsAddTorsionFree` `MulZeroClass.mul_zero` `mul_one`
`constantCoeff_expand` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `constantCoeff` `AlgHom` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`coeff_zero_eq_constantCoeff` `smul_zero` `coeff_expand_smul`
`expand_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`mul_one` `smul_eq_C_mul` `HasSubst.X_pow` `expand.eq_1` `AlgHom.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `instIsScalarTower` `IsScalarTower.right` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`expand_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`substAlgHom_X` `HasSubst.X_pow`
`expand_comp_substAlgHom` 📖	mathematical	`HasSubst`	`AlgHom.comp` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `expand` `substAlgHom` `DFunLike.coe` `AlgHom` `AlgHom.funLike` `HasSubst.expand`	—	`AlgHom.ext` `HasSubst.expand` `HasSubst.X_pow` `coe_substAlgHom` `subst_comp_subst_apply` `IsScalarTower.right` `substAlgHom_apply` `substAlgHom.congr_simp`
`expand_eq_expand` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `MvPolynomial.toMvPowerSeries` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `MvPolynomial.expand`	—	`ext` `Finsupp.ext` `coeff_expand_smul` `MvPolynomial.coeff_expand_smul` `MvPolynomial.coeff_coe` `Mathlib.Tactic.Push.not_forall_eq` `coeff_expand_of_not_dvd` `MvPolynomial.coeff_expand_of_not_dvd`
`expand_monomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instNatSMul` `Nat.instAddMonoid`	—	`HasSubst.X_pow` `expand.eq_1` `substAlgHom_monomial` `monomial_eq'` `Finsupp.prod.eq_1` `Finsupp.prod_of_support_subset` `Finsupp.support_smul` `pow_zero` `algebraMap_apply` `Finset.prod_congr` `pow_mul`
`expand_mul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`DFunLike.congr_fun` `expand_mul_eq_comp`
`expand_mul_eq_comp` 📖	mathematical	—	`expand` `AlgHom.comp` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id`	—	`AlgHom.ext` `HasSubst.X_pow` `pow_mul` `substAlgHom.congr_simp` `substAlgHom_apply` `coe_substAlgHom` `subst_comp_subst_apply` `IsScalarTower.right` `subst_pow` `subst_X`
`expand_one` 📖	mathematical	—	`expand` `one_ne_zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.instOne` `AlgHom.id` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id`	—	`AlgHom.ext` `one_ne_zero` `HasSubst.X_pow` `pow_one` `substAlgHom.congr_simp` `substAlgHom_apply` `subst_self`
`expand_one_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `one_ne_zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.instOne`	—	`one_ne_zero` `expand_one`
`expand_subst` 📖	mathematical	`HasSubst`	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `subst`	—	`substAlgHom_apply` `HasSubst.expand` `expand_substAlgHom`
`expand_substAlgHom` 📖	mathematical	`HasSubst`	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `substAlgHom` `HasSubst.expand`	—	`HasSubst.expand` `AlgHom.comp_apply` `expand_comp_substAlgHom`
`map_expand` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `map` `AlgHom` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`substAlgHom_apply` `HasSubst.X_pow` `map_subst` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_X`
`map_frobenius_expand` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `map` `frobenius` `AlgHom` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eq_iff_frequently_trunc'_eq` `Filter.frequently_atTop` `SemilatticeSup.instIsDirectedOrder` `le_self_nsmul` `IsOrderedAddMonoid.toAddLeftMono` `Finsupp.isOrderedAddMonoid` `Nat.instIsOrderedAddMonoid` `zero_le` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `MvPolynomial.map_expand` `expand_eq_expand` `map_expand` `ext` `MvPolynomial.coeff_map` `trunc'_map` `trunc'_expand` `trunc'_trunc'_pow` `expChar_ne_zero` `MvPolynomial.coe_pow` `MvPolynomial.map_frobenius_expand` `trunc'_expand_trunc'`
`map_iterateFrobenius_expand` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `map` `iterateFrobenius` `AlgHom` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid` `pow_ne_zero` `Nat.instMonoidWithZero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instSemiring` `Nat.instLinearOrder` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instCanonicallyOrderedAdd` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `iterateFrobenius_zero` `pow_zero` `expand.congr_simp` `expand_one` `pow_one` `pow_succ` `pow_mul` `map_frobenius_expand` `pow_succ'` `iterateFrobenius.congr_simp` `add_comm` `iterateFrobenius_add` `iterateFrobenius_one`
`order_expand` 📖	mathematical	—	`order` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `MvPowerSeries` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `ENat` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instCommSemiringENat`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `order_zero` `nsmul_eq_mul` `ENat.mul_top` `Nat.cast_zero` `eq_of_le_of_ge` `exists_coeff_ne_zero_and_order` `ne_zero_iff_order_finite` `map_nsmul` `AddMonoidHom.instAddMonoidHomClass` `Nat.cast_mul` `order_le` `coeff_expand_smul` `le_order` `Finsupp.ext` `coeff_of_lt_order` `lt_of_mul_lt_mul_left'` `contravariant_lt_of_covariant_le` `CanonicallyOrderedAdd.toMulLeftMono` `Mathlib.Tactic.Push.not_forall_eq` `coeff_expand_of_not_dvd`
`support_expand` 📖	mathematical	—	`Function.support` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Set.image` `Finsupp.instNatSMul` `Nat.instAddMonoid`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `support_expand_subset` `coeff_apply` `coeff_expand_smul` `Function.mem_support`
`support_expand_subset` 📖	mathematical	—	`Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.instHasSubset` `Function.support` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Set.image` `Finsupp.instNatSMul` `Nat.instAddMonoid`	—	`by_contra` `coeff_expand_of_not_dvd` `Finsupp.ext` `coeff_apply` `coeff_expand_smul` `Function.mem_support`
`trunc'_expand` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MvPowerSeries` `MvPolynomial` `CommRing.toCommSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AddMonoidHom.instFunLike` `trunc'` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instNatSMul` `Nat.instAddMonoid` `AlgHom` `instSemiring` `instAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `MvPolynomial.algebra` `MvPolynomial.expand`	—	`MvPolynomial.ext` `Finsupp.ext` `Nat.instCanonicallyOrderedAdd` `coeff_trunc'` `nsmul_le_nsmul_right` `IsOrderedAddMonoid.toAddLeftMono` `Finsupp.isOrderedAddMonoid` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `coeff_expand_smul` `MvPolynomial.coeff_expand_smul` `Finsupp.coe_le_coe` `Mathlib.Tactic.Push.not_forall_eq` `MvPolynomial.coeff_expand_of_not_dvd` `coeff_expand_of_not_dvd`
`trunc'_expand_trunc'` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLE`	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.expand` `AddMonoidHom` `MvPowerSeries` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `trunc'` `Finsupp.instNatSMul` `Nat.instAddMonoid` `MvPolynomial.toMvPowerSeries`	—	`expand_eq_expand` `trunc'_expand` `trunc'_trunc'`

MvPowerSeries.HasSubst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expand` 📖	mathematical	`MvPowerSeries.HasSubst`	`DFunLike.coe` `AlgHom` `MvPowerSeries` `CommRing.toCommSemiring` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `AlgHom.funLike` `MvPowerSeries.expand`	—	`comp` `X_pow`

---

← Back to Index