IrreducibleQuadratic

📁 Source: Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean

Statistics

Metric	Count
Definitions instModuleSelf, sumSMulX, sumSMulXSMulY	3
Theorems coeff_sumSMulX, irreducible_mul_X_add, irreducible_of_disjoint_support, irreducible_of_totalDegree_eq_one, irreducible_sumSMulX, irreducible_sumSMulXSMulY	6
Total	9

MvPolynomial

Definitions

Name	Category	Theorems
instModuleSelf 📖	CompOp	3 math math: irreducible_sumSMulX, coeff_sumSMulX, irreducible_sumSMulXSMulY
sumSMulX 📖	CompOp	2 math math: irreducible_sumSMulX, coeff_sumSMulX
sumSMulXSMulY 📖	CompOp	1 math math: irreducible_sumSMulXSMulY

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_sumSMulX 📖	mathematical	—	coeff CommRing.toCommSemiring Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidAlgebra.addAddCommMonoid Finsupp.module Semiring.toModule instModuleSelf LinearMap.instFunLike sumSMulX Finsupp.instFunLike	—	sumSMulX.eq_1 Finsupp.linearCombination_apply Finsupp.sum.eq_1 coeff_sum Finset.sum_eq_single coeff_smul coeff_X' MulZeroClass.mul_zero coeff_single_X mul_one
irreducible_mul_X_add 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike vars CommRing.toCommSemiring IsRelPrime MvPolynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass AddMonoidAlgebra.instMul X	—	algHom_ext ext optionEquivLeft_symm_C_X rename_X exists_rename_eq_of_vars_subset_range Subtype.val_injective Subtype.range_coe_subtype Irreducible.of_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass isLocalHom_equiv RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass rename_rename Equiv.symm_comp_self rename_id AlgEquiv.apply_symm_apply optionEquivLeft_X_none Polynomial.irreducible_C_mul_X_add_C instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsRelPrime.of_map NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Polynomial.instIsLocalHomRingHomC
irreducible_of_disjoint_support 📖	mathematical	Finset.Nontrivial Finsupp MulZeroClass.toZero Nat.instMulZeroClass support CommRing.toCommSemiring Finset SetLike.instMembership Finset.instSetLike DFunLike.coe Finsupp.instFunLike Set.PairwiseDisjoint Finset.partialOrder Finset.instOrderBot SetLike.coe Finsupp.support IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid	—	Finsupp.erase_add_single monomial_add_single pow_one coeff_sub coeff_monomial ite_add_ite zero_add add_zero irreducible_mul_X_add vars_monomial Finsupp.support_erase Finset.disjoint_iff_ne dvd_monomial_iff_exists IsDomain.to_noZeroDivisors Finset.Nontrivial.exists_ne coeff_add coeff_C_mul MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass instIsLocalHomRingHomC Finsupp.support_mono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_monomial_mul' HasSubset.Subset.trans Finset.instIsTransSubset Finset.erase_subset
irreducible_of_totalDegree_eq_one 📖	mathematical	totalDegree CommRing.toCommSemiring IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid	—	isUnit_iff_totalDegree_of_isReduced isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors eq_or_ne MulZeroClass.zero_mul totalDegree_zero MulZeroClass.mul_zero totalDegree_mul_of_isDomain totalDegree_eq_zero_iff_eq_C MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass instIsLocalHomRingHomC coeff_C_mul mul_comm
irreducible_sumSMulX 📖	mathematical	Finset.Nonempty Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidAlgebra.addAddCommMonoid Finsupp.module Semiring.toModule instModuleSelf LinearMap.instFunLike sumSMulX	—	irreducible_of_totalDegree_eq_one le_antisymm Finset.sum_congr totalDegree_finsetSum_le le_trans totalDegree_smul_le totalDegree_X IsDomain.toNontrivial instReflLe not_lt totalDegree_eq_zero_iff Finsupp.single_eq_same mem_support_iff coeff_sumSMulX
irreducible_sumSMulXSMulY 📖	mathematical	Finset.Nontrivial Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Irreducible MvPolynomial CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidAlgebra.addAddCommMonoid Finsupp.module Semiring.toModule instModuleSelf LinearMap.instFunLike sumSMulXSMulY	—	Finsupp.single_apply add_zero zero_add Finsupp.sum_single monomial_mul mul_one smul_monomial Finsupp.sum_embDomain Finsupp.embDomain_apply Function.instEmbeddingLikeEmbedding Classical.choose_eq support.eq_1 Finsupp.support_embDomain Finset.Nontrivial.nonempty irreducible_of_disjoint_support Finset.map_nontrivial mem_support_iff Finsupp.mem_support_iff Finsupp.single_eq_same Finsupp.single_eq_of_ne Finset.coe_map Set.InjOn.pairwiseDisjoint_image Function.Injective.injOn Function.Embedding.injective Finsupp.support_add_eq Finsupp.support_single_ne_zero

---

← Back to Index