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 CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.mul IsScalarTower.right Submodule.instPowNat natDegree coeff 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 Ring.toSemiring 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 CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.mul IsScalarTower.right Submodule.instPowNat natDegree coeff 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	—	Ideal.span Polynomial CommSemiring.toSemiring CommRing.toCommSemiring 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