CoeffMulMem

📁 Source: Mathlib/RingTheory/PowerSeries/CoeffMulMem.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', coeff_mul_mem_ideal_of_coeff_left_mem_ideal, coeff_mul_mem_ideal_of_coeff_left_mem_ideal', coeff_mul_mem_ideal_of_coeff_right_mem_ideal, coeff_mul_mem_ideal_of_coeff_right_mem_ideal'	6
Total	6

PowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries instAddCommMonoid instModule LinearMap.instFunLike coeff	Submodule.mul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction MvPowerSeries.instMul	—	IsScalarTower.left coeff_mul Ideal.sum_mem Ideal.mul_mem_mul LE.le.trans Finset.antidiagonal.fst_le Nat.instCanonicallyOrderedAdd Finset.antidiagonal.snd_le
coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries instAddCommMonoid instModule LinearMap.instFunLike coeff	Submodule.mul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction MvPowerSeries.instMul	—	coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal le_rfl
coeff_mul_mem_ideal_of_coeff_left_mem_ideal 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries instAddCommMonoid instModule LinearMap.instFunLike coeff	MvPowerSeries.instMul	—	IsScalarTower.left Ideal.IsTwoSided.mul_one coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal Ideal.one_eq_top
coeff_mul_mem_ideal_of_coeff_left_mem_ideal' 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries instAddCommMonoid instModule LinearMap.instFunLike coeff	MvPowerSeries.instMul	—	IsScalarTower.left Ideal.IsTwoSided.mul_one coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' Ideal.one_eq_top
coeff_mul_mem_ideal_of_coeff_right_mem_ideal 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries instAddCommMonoid instModule LinearMap.instFunLike coeff	MvPowerSeries.instMul	—	IsScalarTower.left Ideal.top_mul coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal
coeff_mul_mem_ideal_of_coeff_right_mem_ideal' 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries instAddCommMonoid instModule LinearMap.instFunLike coeff	MvPowerSeries.instMul	—	IsScalarTower.left Ideal.top_mul coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'

---

← Back to Index