MvPolynomial

📁 Source: Mathlib/RingTheory/MvPolynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems finrank_eq_one, finrank_eq_zero, quotient_mk_comp_C_injective, rank_eq, rank_eq_lift	5
Total	5

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_eq_one 📖	mathematical	—	Module.finrank MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module Semiring.toModule	—	Module.rank_eq_one_iff_finrank_eq_one subsingleton_or_nontrivial rank_subsingleton rank_eq_lift Cardinal.mk_fintype Fintype.card_unique Nat.cast_one Cardinal.lift_one
finrank_eq_zero 📖	mathematical	—	Module.finrank MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module Semiring.toModule	—	LinearIndependent.finrank_eq_zero_of_infinite Finsupp.infinite_of_right instInfiniteNat Module.Basis.linearIndependent
quotient_mk_comp_C_injective 📖	mathematical	—	HasQuotient.Quotient MvPolynomial Semifield.toCommSemiring Field.toSemifield Ideal Ring.toSemiring CommRing.toRing instCommRingMvPolynomial EuclideanDomain.toCommRing Field.toEuclideanDomain Ideal.instHasQuotient DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike RingHom.comp C	—	Ideal.instIsTwoSided_1 injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass by_contradiction Ideal.eq_top_iff_one Ideal.mul_mem_left Ideal.Quotient.eq_zero_iff_mem RingHom.comp_apply C_1 inv_mul_cancel₀ RingHom.map_mul
rank_eq 📖	mathematical	—	Module.rank MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module Semiring.toModule Finsupp MulZeroClass.toZero Nat.instMulZeroClass	—	Module.Basis.mk_eq_rank commRing_strongRankCondition
rank_eq_lift 📖	mathematical	—	Module.rank MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module Semiring.toModule Cardinal.lift Finsupp MulZeroClass.toZero Nat.instMulZeroClass	—	Module.Basis.mk_eq_rank commRing_strongRankCondition Cardinal.lift_lift Cardinal.lift_umax

---

← Back to Index