MvPolynomial

📁 Source: Mathlib/RingTheory/MvPolynomial.lean

Statistics

Metric	Count
Definitions instModule	1
Theorems finrank_eq_one, finrank_eq_zero, quotient_mk_comp_C_injective, rank_eq, rank_eq_lift	5
Total	6

MvPolynomial

Definitions

Name	Category	Theorems
instModule 📖	CompOp	3 math math: finrank_eq_zero, MvRatFunc.rank_eq_max_lift, finrank_eq_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_eq_one 📖	mathematical	—	Module.finrank MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule	—	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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule	—	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 AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass DivisionRing.toRing Field.toDivisionRing Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 AddMonoidAlgebra.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Finsupp.instAddCommMonoid Nat.instAddCommMonoid 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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddMonoidAlgebra.module Semiring.toModule	—	Module.Basis.mk_eq_rank commRing_strongRankCondition
rank_eq_lift 📖	mathematical	—	Module.rank MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddMonoidAlgebra.module Semiring.toModule Cardinal.lift	—	Module.Basis.mk_eq_rank commRing_strongRankCondition Cardinal.lift_lift Cardinal.lift_umax

---

← Back to Index