Documentation Verification Report

ChevalleyComplexity

📁 Source: Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean

Statistics

Metric	Count
Definitions `degBound`, `numBound`, `degBound`, `numBound`	4
Theorems `degBound_casesOn_succ`, `degBound_le_degBound`, `degBound_pos`, `degBound_succ`, `degBound_zero`, `numBound_casesOn_succ`, `numBound_mono`, `numBound_succ`, `numBound_zero`, `chevalley_mvPolynomialC`, `chevalley_polynomialC`, `chevalley_mvPolynomial_mvPolynomial`	12
Total	16

ChevalleyThm

Definitions

Name	Category	Theorems
`degBound` 📖	CompOp	1 math math: `chevalley_mvPolynomial_mvPolynomial`
`numBound` 📖	CompOp	1 math math: `chevalley_mvPolynomial_mvPolynomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chevalley_mvPolynomialC` 📖	mathematical	`Submodule` `Int.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `PrimeSpectrum.BasicConstructibleSetData.n` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Int.instCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `MvPolynomial.module` `Submodule.instMin` `MvPolynomial.coeffsIn` `Submodule.restrictScalars` `Semiring.toModule` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroup.intIsScalarTower` `MvPolynomial.instCommRingMvPolynomial` `Ring.toSemiring` `MvPolynomial.degreesLE` `PrimeSpectrum.BasicConstructibleSetData.g`	`Set.image` `PrimeSpectrum` `PrimeSpectrum.comap` `MvPolynomial.C` `PrimeSpectrum.ConstructibleSetData.toSet` `MvPolynomialC.numBound` `Multiset.count` `Multiset.map` `Submodule.instPowNat` `IsScalarTower.right` `Ring.toIntAlgebra` `MvPolynomialC.degBound`	—	`AddCommGroup.intIsScalarTower` `IsScalarTower.right` `Fin.isEmpty'` `PrimeSpectrum.ConstructibleSetData.toSet_map` `OrderIso.image_eq_preimage_symm` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `MvPolynomial.isEmptyRingEquiv_eq_coeff_zero` `MvPolynomialC.numBound_zero` `MvPolynomialC.degBound_zero` `pow_one` `Finset.sup_le` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Nat.instCanonicallyOrderedAdd` `MvPolynomial.degree_finSuccEquiv` `WithBot.succ_natCast` `add_comm` `MvPolynomial.degreeOf_def` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Multiset.count_le_of_le` `Finset.sum_const` `Fintype.card_fin` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `Function.Injective.injOn` `Fin.succ_injective` `chevalley_polynomialC` `MvPolynomial.degrees_one` `Multiset.instCanonicallyOrderedAdd` `MvPolynomial.finSuccEquiv_coeff_coeff` `Finsupp.count_toMultiset` `LE.le.trans` `MvPolynomial.degreeOf_coeff_finSuccEquiv` `SetLike.le_def` `instIsConcreteLE` `pow_inf_le` `Submodule.instMulLeftMono` `Submodule.instMulRightMono` `inf_le_inf` `pow_le_pow_right'` `Nat.pow_self_mono` `MvPolynomial.le_coeffsIn_pow` `MvPolynomial.degreesLE_nsmul` `Submodule.restrictScalars_pow` `LT.lt.ne'` `Submodule.one_le` `le_self_pow` `Multiset.count_map_eq_count'` `Fin.val_injective` `le_rfl` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `Set.image_comp` `PrimeSpectrum.comap_comp` `Set.image_image` `Set.image_congr` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Multiset.count.congr_simp` `Multiset.map_nsmul` `Multiset.count_nsmul` `MvPolynomialC.numBound_mono` `mul_add` `Distrib.leftDistribClass` `mul_one` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Eq.trans_le` `MvPolynomialC.numBound_casesOn_succ` `MvPolynomialC.degBound_le_degBound` `MvPolynomialC.degBound_casesOn_succ`
`chevalley_polynomialC` 📖	mathematical	`Submodule` `Int.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PrimeSpectrum.BasicConstructibleSetData.g` `Polynomial`	`Set.image` `PrimeSpectrum` `Polynomial.commSemiring` `PrimeSpectrum.comap` `Polynomial.C` `PrimeSpectrum.ConstructibleSetData.toSet` `PrimeSpectrum.BasicConstructibleSetData.n` `PrimeSpectrum.ConstructibleSetData.degBound` `Submodule.instPowNat` `IsScalarTower.right` `Int.instCommSemiring` `Ring.toSemiring` `Ring.toIntAlgebra` `Monoid.toNatPow` `Nat.instMonoid`	—	`IsScalarTower.right` `Set.iUnion_congr_Prop` `Set.image_iUnion` `Finset.set_biUnion_biUnion` `Finset.le_sup` `LE.le.trans` `SetLike.le_def` `instIsConcreteLE` `pow_le_pow` `Submodule.instMulLeftMono` `Submodule.instMulRightMono` `Submodule.span_le` `Submodule.one_eq_span` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `sub_eq_zero_of_eq` `le_refl` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul`

ChevalleyThm.MvPolynomialC

Definitions

Name	Category	Theorems
`degBound` 📖	CompOp	7 math math: `degBound_casesOn_succ`, `numBound_succ`, `ChevalleyThm.chevalley_mvPolynomialC`, `degBound_pos`, `degBound_succ`, `degBound_zero`, `degBound_le_degBound`
`numBound` 📖	CompOp	6 math math: `numBound_zero`, `numBound_succ`, `ChevalleyThm.chevalley_mvPolynomialC`, `numBound_mono`, `degBound_succ`, `numBound_casesOn_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degBound_casesOn_succ` 📖	mathematical	—	`degBound` `Monoid.toNatPow` `Nat.instMonoid` `AddMonoid.toNatSMul` `Pi.addMonoid` `Nat.instAddMonoid`	—	—
`degBound_le_degBound` 📖	mathematical	—	`degBound`	—	—
`degBound_pos` 📖	mathematical	—	`degBound`	—	`degBound_zero` `Nat.instZeroLEOneClass` `degBound_succ` `numBound_succ` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`degBound_succ` 📖	mathematical	—	`degBound` `Monoid.toNatPow` `Nat.instMonoid` `numBound`	—	`degBound.eq_2`
`degBound_zero` 📖	mathematical	—	`degBound`	—	`degBound.eq_1`
`numBound_casesOn_succ` 📖	mathematical	—	`numBound` `AddMonoid.toNatSMul` `Pi.addMonoid` `Nat.instAddMonoid` `Monoid.toNatPow` `Nat.instMonoid`	—	—
`numBound_mono` 📖	mathematical	—	`numBound`	—	—
`numBound_succ` 📖	mathematical	—	`numBound` `degBound`	—	`numBound.eq_2`
`numBound_zero` 📖	mathematical	—	`numBound`	—	`numBound.eq_1`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chevalley_mvPolynomial_mvPolynomial` 📖	mathematical	`PrimeSpectrum.BasicConstructibleSetData.n` `MvPolynomial` `CommRing.toCommSemiring` `Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `MvPolynomial.degrees` `PrimeSpectrum.BasicConstructibleSetData.g` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.X`	`Set.image` `PrimeSpectrum` `PrimeSpectrum.comap` `RingHomClass.toRingHom` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `PrimeSpectrum.ConstructibleSetData.toSet` `ChevalleyThm.numBound` `MvPolynomial.degreeOf` `ChevalleyThm.degBound`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MvPolynomial.ringHom_ext'` `RingHom.ext` `MvPolynomial.eval₂_C` `MvPolynomial.algHom_C` `MvPolynomial.ext` `MvPolynomial.map_C` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids` `MvPolynomial.map_X` `MvPolynomial.eval₂_X` `DFunLike.congr_fun` `Function.LeftInverse.surjective` `RingHom.instRingHomClass` `range_comap_of_surjective` `PrimeSpectrum.zeroLocus_span` `map_sub` `RingHomClass.toAddMonoidHomClass` `MvPolynomial.eval₂Hom_C` `sub_self` `LE.le.antisymm` `AlgEquiv.surjective` `AlgEquiv.injective` `AlgEquiv.symm_apply_apply` `MvPolynomial.induction_on` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `MvPolynomial.commAlgEquiv_C` `zero_add` `AlgEquiv.apply_symm_apply` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `add_add_add_comm` `AddMonoidHomClass.toAddHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MvPolynomial.commAlgEquiv_X` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Ideal.mul_mem_left` `Ideal.subset_span` `Set.mem_range_self` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `add_zero` `Set.injOn_preimage` `Set.Subset.rfl` `Set.preimage_range` `Set.preimage_image_eq` `PrimeSpectrum.comap_injective_of_surjective` `Set.preimage_inter` `Set.inter_univ` `Set.preimage_comp` `PrimeSpectrum.comap_comp` `Set.iUnion_congr_Prop` `Set.image_iUnion₂` `Set.image_diff` `Finset.set_biUnion_finset_image` `Set.range_comp` `Equiv.range_eq_univ` `Set.image_univ` `Set.Sum.elim_range` `PrimeSpectrum.zeroLocus_union` `PrimeSpectrum.preimage_comap_zeroLocus` `Set.image_singleton` `Set.sdiff_inter_right_comm` `IsScalarTower.right` `AddCommGroup.intIsScalarTower` `ChevalleyThm.chevalley_mvPolynomialC` `MvPolynomial.degrees_one` `Multiset.instCanonicallyOrderedAdd` `Finset.forall_mem_image` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Equiv.surjective` `Equiv.symm_apply_apply` `MvPolynomial.coeff_map` `MvPolynomial.degrees_C` `MvPolynomial.coeff_sub` `MvPolynomial.coeff_C` `LE.le.trans` `MvPolynomial.degrees_sub_le` `MvPolynomial.degrees_zero` `Multiset.union_zero` `MvPolynomial.degrees_X'` `MvPolynomial.degrees_map_le` `Multiset.zero_union` `Set.image_comp` `Multiset.count_nsmul` `Multiset.count_univ` `mul_one` `Multiset.le_iff_count` `MvPolynomial.mem_degreesLE` `Submodule.restrictScalars_mem` `MvPolynomial.degreesLE_nsmul` `Submodule.restrictScalars_pow` `LT.lt.ne'` `ChevalleyThm.MvPolynomialC.degBound_pos`

---

← Back to Index