Init

📁 Source: Mathlib/RingTheory/DividedPowerAlgebra/Init.lean

Statistics

Metric	Count
Definitions `DividedPowerAlgebra`, `RelI`, `dp`, `embed`	4
Theorems `algHom_ext`, `algHom_ext_iff`, `dp_add`, `dp_def`, `dp_eq_mkRingHom`, `dp_mul`, `dp_null`, `dp_null_of_ne_zero`, `dp_smul`, `dp_sum`, `dp_sum_smul`, `dp_zero`, `embed_def`, `induction_on`, `induction_on'`, `mkAlgHom_C`, `mkAlgHom_surjective`, `mkRingHom_C`, `natFactorial_mul_dp_eq`, `prod_dp`, `submodule_span_prod_dp_eq_top`	21
Total	25

DividedPowerAlgebra

Definitions

Name	Category	Theorems
`RelI` 📖	CompOp	—
`dp` 📖	CompOp	15 math math: `dp_mul`, `natFactorial_mul_dp_eq`, `dp_zero`, `submodule_span_prod_dp_eq_top`, `algHom_ext_iff`, `dp_sum_smul`, `dp_def`, `dp_sum`, `dp_smul`, `dp_add`, `dp_null_of_ne_zero`, `prod_dp`, `embed_def`, `dp_eq_mkRingHom`, `dp_null`
`embed` 📖	CompOp	1 math math: `embed_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`DFunLike.coe` `AlgHom` `DividedPowerAlgebra` `RingQuot.instSemiring` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `dp`	—	—	`algHom_ext_iff`
`algHom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `DividedPowerAlgebra` `RingQuot.instSemiring` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `dp`	—	`DFunLike.ext'_iff` `Function.Surjective.injective_comp_right` `mkAlgHom_surjective` `MvPolynomial.algHom_ext`
`dp_add` 📖	mathematical	—	`dp` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Finset.sum` `DividedPowerAlgebra` `RingQuot.instAddCommMonoid` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Finset.HasAntidiagonal.antidiagonal` `Finset.Nat.instHasAntidiagonal` `RingQuot.instMul`	—	`Finset.sum_congr` `RingQuot.mkAlgHom_rel` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass`
`dp_def` 📖	mathematical	—	`dp` `DFunLike.coe` `AlgHom` `MvPolynomial` `RingQuot` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instSemiring` `AddMonoidAlgebra.algebra` `Algebra.id` `RingQuot.instAlgebra` `AlgHom.funLike` `RingQuot.mkAlgHom` `MvPolynomial.X`	—	—
`dp_eq_mkRingHom` 📖	mathematical	—	`dp` `DFunLike.coe` `RingHom` `MvPolynomial` `RingQuot` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Semiring.toNonAssocSemiring` `RingQuot.instSemiring` `RingHom.instFunLike` `RingQuot.mkRingHom` `MvPolynomial.X`	—	`RingQuot.mkRingHom_def` `RingQuot.mkAlgHom_def`
`dp_mul` 📖	mathematical	—	`DividedPowerAlgebra` `RingQuot.instMul` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `dp` `AddMonoid.toNSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `RingQuot.instSemiring` `Nat.choose`	—	`NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `RingQuot.mkAlgHom_rel`
`dp_null` 📖	mathematical	—	`dp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DividedPowerAlgebra` `RingQuot.instOne` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instZero`	—	`dp_zero` `ne_of_gt` `zero_smul` `dp_smul` `zero_pow`
`dp_null_of_ne_zero` 📖	mathematical	—	`dp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DividedPowerAlgebra` `RingQuot.instZero` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel`	—	`dp_null`
`dp_smul` 📖	mathematical	—	`dp` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `DividedPowerAlgebra` `RingQuot.instSMulOfAlgebra` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `AddMonoidAlgebra.algebra` `Algebra.id` `Monoid.toPow`	—	`dp_def` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `RingQuot.mkAlgHom_rel`
`dp_sum` 📖	mathematical	—	`dp` `Finset.sum` `Sym` `DividedPowerAlgebra` `RingQuot.instAddCommMonoid` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Finset.sym` `Finset.prod` `CommSemiring.toCommMonoid` `RingQuot.instCommSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Multiset.count` `Sym.toMultiset`	—	`DividedPowers.dpow_sum'` `dp_zero` `dp_add` `dp_null_of_ne_zero`
`dp_sum_smul` 📖	mathematical	—	`dp` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Sym` `DividedPowerAlgebra` `RingQuot.instAddCommMonoid` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Finset.sym` `RingQuot.instSMulOfAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id` `Finset.prod` `CommSemiring.toCommMonoid` `Monoid.toPow` `Multiset.count` `Sym.toMultiset` `RingQuot.instCommSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`dp_sum` `Finset.sum_congr` `Finset.prod_congr` `dp_smul` `Algebra.smul_def` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`dp_zero` 📖	mathematical	—	`dp` `DividedPowerAlgebra` `RingQuot.instOne` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel`	—	`dp_def` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingQuot.mkAlgHom_rel`
`embed_def` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DividedPowerAlgebra` `RingQuot.instAddCommMonoid` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Algebra.toModule` `RingQuot.instSemiring` `RingQuot.instAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id` `LinearMap.instFunLike` `embed` `dp`	—	—
`induction_on` 📖	—	`DFunLike.coe` `RingHom` `DividedPowerAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingQuot.instSemiring` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingHom.instFunLike` `algebraMap` `RingQuot.instAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id` `RingQuot.instAdd` `RingQuot.instMul` `dp`	—	—	`induction_on'` `mkAlgHom_C`
`induction_on'` 📖	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `RingQuot` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instSemiring` `AddMonoidAlgebra.algebra` `Algebra.id` `RingQuot.instAlgebra` `AlgHom.funLike` `RingQuot.mkAlgHom` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `MvPolynomial.C` `DividedPowerAlgebra` `RingQuot.instAdd` `RingQuot.instMul` `dp`	—	—	`RingQuot.mkRingHom_surjective` `MvPolynomial.induction_on` `RingQuot.mkAlgHom_def` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`mkAlgHom_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `RingQuot` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instSemiring` `AddMonoidAlgebra.algebra` `Algebra.id` `RingQuot.instAlgebra` `AlgHom.funLike` `RingQuot.mkAlgHom` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `MvPolynomial.C` `DividedPowerAlgebra` `algebraMap`	—	`MvPolynomial.algebraMap_eq` `AlgHom.commutes`
`mkAlgHom_surjective` 📖	mathematical	—	`MvPolynomial` `RingQuot` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `DFunLike.coe` `AlgHom` `RingQuot.instSemiring` `AddMonoidAlgebra.algebra` `Algebra.id` `RingQuot.instAlgebra` `AlgHom.funLike` `RingQuot.mkAlgHom`	—	`RingQuot.mkAlgHom_surjective`
`mkRingHom_C` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `RingQuot` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Semiring.toNonAssocSemiring` `RingQuot.instSemiring` `RingHom.instFunLike` `RingQuot.mkRingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `MvPolynomial.C` `DividedPowerAlgebra` `algebraMap` `RingQuot.instAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id`	—	`mkAlgHom_C` `RingQuot.mkAlgHom_def`
`natFactorial_mul_dp_eq` 📖	mathematical	—	`DividedPowerAlgebra` `RingQuot.instMul` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `RingQuot.instNatCast` `Nat.factorial` `dp` `Monoid.toPow` `MonoidWithZero.toMonoid` `RingQuot.instMonoidWithZero`	—	`Nat.cast_one` `dp_zero` `mul_one` `pow_zero` `pow_succ` `mul_assoc` `dp_mul` `nsmul_eq_mul` `Nat.cast_mul` `Nat.cast_add` `Nat.choose_succ_self_right` `mul_comm`
`prod_dp` 📖	mathematical	—	`Finset.prod` `DividedPowerAlgebra` `CommSemiring.toCommMonoid` `RingQuot.instCommSemiring` `MvPolynomial` `AddMonoidAlgebra.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Rel` `dp` `RingQuot.instMul` `AddMonoidAlgebra.semiring` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `RingQuot.instNatCast` `Nat.multinomial` `Finset.sum`	—	`Finset.induction` `Nat.multinomial_empty` `Nat.cast_one` `dp_zero` `one_mul` `Finset.prod_insert` `mul_assoc` `mul_comm` `dp_mul` `Finset.sum_insert` `nsmul_eq_mul` `Nat.multinomial_insert` `Nat.cast_mul`
`submodule_span_prod_dp_eq_top` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Submodule.span` `DividedPowerAlgebra` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `CommSemiring.toSemiring` `RingQuot.instAddCommMonoid` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Rel` `Algebra.toModule` `RingQuot.instSemiring` `RingQuot.instAlgebra` `AddMonoidAlgebra.algebra` `Algebra.id` `Set.range` `Finsupp.prod` `CommRing.toCommMonoid` `RingQuot.instCommRing` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `dp` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `induction_on` `Algebra.algebraMap_eq_smul_one` `Submodule.smul_mem` `Submodule.subset_span` `Submodule.add_mem` `Submodule.span_induction` `Finsupp.mul_prod_erase'` `dp_zero` `mul_comm` `mul_assoc` `dp_mul` `nsmul_eq_mul` `Submodule.smul_of_tower_mem` `AddCommMonoid.nat_isScalarTower` `Submodule.mem_span_of_mem` `Finsupp.single_eq_same` `Finsupp.erase_add` `Finsupp.erase_single` `zero_add` `MulZeroClass.zero_mul` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `add_mul` `Distrib.rightDistribClass` `smul_mul_assoc` `IsScalarTower.right` `dp_null` `mul_one` `MulZeroClass.mul_zero` `dp_add` `Finset.mul_sum` `sum_mem` `dp_smul` `Algebra.mul_smul_comm`

(root)

Definitions

Name	Category	Theorems
`DividedPowerAlgebra` 📖	CompOp	15 math math: `DividedPowerAlgebra.dp_mul`, `DividedPowerAlgebra.natFactorial_mul_dp_eq`, `DividedPowerAlgebra.dp_zero`, `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`, `DividedPowerAlgebra.algHom_ext_iff`, `DividedPowerAlgebra.dp_sum_smul`, `DividedPowerAlgebra.dp_sum`, `DividedPowerAlgebra.dp_smul`, `DividedPowerAlgebra.dp_add`, `DividedPowerAlgebra.dp_null_of_ne_zero`, `DividedPowerAlgebra.mkRingHom_C`, `DividedPowerAlgebra.prod_dp`, `DividedPowerAlgebra.mkAlgHom_C`, `DividedPowerAlgebra.embed_def`, `DividedPowerAlgebra.dp_null`

---

← Back to Index