Monomial

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

Statistics

Metric	Count
Definitions	0
Theorems card_support_le_one_iff_monomial, infinite, monomial_one_eq_iff, ringHom_ext, ringHom_ext', ringHom_ext'_iff	6
Total	6

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_support_le_one_iff_monomial 📖	mathematical	—	Finset.card support DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial	—	Finset.card_le_one_iff_subset_singleton ext coeff_monomial_same notMem_support_iff Finset.mem_singleton coeff_monomial Finset.card_singleton Finset.card_le_card support_monomial'
infinite 📖	mathematical	—	Infinite Polynomial	—	Infinite.of_injective instInfiniteNat
monomial_one_eq_iff 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	AddMonoidAlgebra.of_injective
ringHom_ext 📖	—	DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X	—	—	AddMonoidAlgebra.ringHom_ext' RingHom.ext ofFinsupp_single MonoidHom.ext_mnat MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.comp_assoc RingEquiv.symm_apply_apply
ringHom_ext' 📖	—	RingHom.comp Polynomial Semiring.toNonAssocSemiring semiring C DFunLike.coe RingHom RingHom.instFunLike X	—	—	ringHom_ext RingHom.congr_fun
ringHom_ext'_iff 📖	mathematical	—	RingHom.comp Polynomial Semiring.toNonAssocSemiring semiring C DFunLike.coe RingHom RingHom.instFunLike X	—	ringHom_ext'

---

← Back to Index