Documentation Verification Report

IrreducibleQuadratic

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

Statistics

Metric	Count
Definitions `sumSMulX`, `sumSMulXSMulY`	2
Theorems `coeff_sumSMulX`, `irreducible_mul_X_add`, `irreducible_of_disjoint_support`, `irreducible_of_totalDegree_eq_one`, `irreducible_sumSMulX`, `irreducible_sumSMulXSMulY`	6
Total	8

MvPolynomial

Definitions

Name	Category	Theorems
`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` `instCommRingMvPolynomial` `Finsupp.module` `Semiring.toModule` `module` `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` `Finset.instMembership` `vars` `CommRing.toCommSemiring` `IsRelPrime` `MvPolynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring`	`Irreducible` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `Distrib.toMul` `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` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `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` `Finset.instMembership` `DFunLike.coe` `Finsupp.instFunLike` `Set.PairwiseDisjoint` `Finset.partialOrder` `Finset.instOrderBot` `SetLike.coe` `Finset.instSetLike` `Finsupp.support` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Irreducible` `MvPolynomial` `commSemiring`	—	`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` `commSemiring`	—	`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` `commSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instCommRingMvPolynomial` `Finsupp.module` `Semiring.toModule` `module` `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` `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` `commSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instCommRingMvPolynomial` `Finsupp.module` `Semiring.toModule` `module` `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