CoeffMem

📁 Source: Mathlib/Algebra/Polynomial/CoeffMem.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_divByMonic_mem_pow_natDegree_mul, coeff_divModByMonicAux_mem_span_pow_mul_span, coeff_modByMonic_mem_pow_natDegree_mul, idealSpan_range_update_divByMonic	4
Total	4

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_divByMonic_mem_pow_natDegree_mul 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike coeff AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Submodule.mul IsScalarTower.right Submodule.instPowNat natDegree divByMonic	—	IsScalarTower.right SetLike.le_def instIsConcreteLE mul_le_mul' Submodule.instMulLeftMono Submodule.instMulRightMono pow_le_pow_left₀ IsOrderedRing.toPosMulMono Submodule.instIsOrderedRing IsOrderedRing.toMulPosMono zero_le Submodule.instCanonicallyOrderedAdd sup_le coeff_divModByMonicAux_mem_span_pow_mul_span AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
coeff_divModByMonicAux_mem_span_pow_mul_span 📖	mathematical	Monic Ring.toSemiring	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule SetLike.instMembership Submodule.setLike Submodule.mul IsScalarTower.right Submodule.instPowNat SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Submodule.one Submodule.span Set.range coeff natDegree Polynomial divModByMonicAux	—	—
coeff_modByMonic_mem_pow_natDegree_mul 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike coeff AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Submodule.mul IsScalarTower.right Submodule.instPowNat natDegree modByMonic	—	IsScalarTower.right SetLike.le_def instIsConcreteLE mul_le_mul' Submodule.instMulLeftMono Submodule.instMulRightMono pow_le_pow_left₀ IsOrderedRing.toPosMulMono Submodule.instIsOrderedRing IsOrderedRing.toMulPosMono zero_le Submodule.instCanonicallyOrderedAdd sup_le coeff_divModByMonicAux_mem_span_pow_mul_span one_mul one_pow Submodule.mul_mem_mul Submodule.pow_mem_pow
idealSpan_range_update_divByMonic 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	Ideal.span Polynomial semiring Set.range Function.update modByMonic CommRing.toRing	—	modByMonic_eq_sub_mul_div mul_comm smul_eq_mul Ideal.span.eq_1 Submodule.span_range_update_sub_smul

---

← Back to Index