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 MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.mul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff 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 MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.mul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff 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 MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.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 MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.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 MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.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 MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id PowerSeries MvPowerSeries.instAddCommMonoid MvPowerSeries.instModule LinearMap.instFunLike coeff MvPowerSeries.instMul	—	IsScalarTower.left Ideal.top_mul coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'

---

← Back to Index