Documentation Verification Report

Polynomial

📁 Source: Mathlib/FieldTheory/Finite/Polynomial.lean

Statistics

Metric	Count
Definitions `R`, `decidableRestrictDegree`, `evalᵢ`, `evalₗ`, `indicator`, `instAddCommGroupR`, `instInhabitedR`, `instModuleR`	8
Theorems `C_dvd_iff_zmod`, `degrees_indicator`, `eq_zero_of_eval_eq_zero`, `eval_indicator_apply_eq_one`, `eval_indicator_apply_eq_zero`, `evalₗ_apply`, `expand_zmod`, `finrank_R`, `frobenius_zmod`, `indicator_mem_restrictDegree`, `instFiniteDimensionalROfFinite`, `ker_evalₗ`, `map_restrict_dom_evalₗ`, `range_evalᵢ`, `rank_R`	15
Total	23

MvPolynomial

Definitions

Name	Category	Theorems
`R` 📖	CompOp	5 math math: `rank_R`, `finrank_R`, `ker_evalₗ`, `instFiniteDimensionalROfFinite`, `range_evalᵢ`
`decidableRestrictDegree` 📖	CompOp	—
`evalᵢ` 📖	CompOp	2 math math: `ker_evalₗ`, `range_evalᵢ`
`evalₗ` 📖	CompOp	2 math math: `map_restrict_dom_evalₗ`, `evalₗ_apply`
`indicator` 📖	CompOp	4 math math: `eval_indicator_apply_eq_one`, `indicator_mem_restrictDegree`, `degrees_indicator`, `eval_indicator_apply_eq_zero`
`instAddCommGroupR` 📖	CompOp	5 math math: `rank_R`, `finrank_R`, `ker_evalₗ`, `instFiniteDimensionalROfFinite`, `range_evalᵢ`
`instInhabitedR` 📖	CompOp	—
`instModuleR` 📖	CompOp	5 math math: `rank_R`, `finrank_R`, `ker_evalₗ`, `instFiniteDimensionalROfFinite`, `range_evalᵢ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_dvd_iff_zmod` 📖	mathematical	—	`MvPolynomial` `Int.instCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `AddMonoidAlgebra.nonUnitalSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `AddMonoid.toAddSemigroup` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C` `ZMod` `CommRing.toCommSemiring` `ZMod.commRing` `map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd`	—	`C_dvd_iff_map_hom_eq_zero` `CharP.intCast_eq_zero_iff` `ZMod.charP`
`degrees_indicator` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `CommRing.toCommSemiring` `indicator` `Finset.sum` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `Finset.univ` `AddMonoid.toNSMul` `AddCommMonoid.toAddMonoid` `Fintype.card` `Multiset.instSingleton`	—	`indicator.eq_1` `LE.le.trans` `degrees_prod_le` `Finset.sum_le_sum` `Multiset.instAddLeftMono` `degrees_sub_le` `degrees_one` `Multiset.zero_union` `le_trans` `degrees_pow_le` `nsmul_le_nsmul_right` `covariant_swap_add_of_covariant_add` `degrees_C` `Multiset.union_zero` `degrees_X'`
`eq_zero_of_eval_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictDegree` `Fintype.card`	`MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`Submodule.mem_bot` `ker_evalₗ`
`eval_indicator_apply_eq_one` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `indicator` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Fintype.one_lt_card` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finset.prod_congr` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `map_pow` `eval_X` `eval_C` `sub_self` `zero_pow` `LT.lt.ne'` `sub_zero` `Finset.prod_const_one`
`eval_indicator_apply_eq_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `indicator` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finset.prod_congr` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `map_pow` `eval_X` `eval_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `Finset.mem_univ` `FiniteField.pow_card_sub_one_eq_one` `sub_eq_zero` `sub_self`
`evalₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `AddMonoidAlgebra.addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra.module` `Semiring.toModule` `Pi.Function.module` `LinearMap.instFunLike` `evalₗ` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `RingHom.instFunLike` `eval`	—	—
`expand_zmod` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ZMod` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `ZMod.instField` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`instExpChar` `expChar_prime` `ZMod.charP` `frobenius_zmod`
`finrank_R` 📖	mathematical	—	`Module.finrank` `R` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `instAddCommGroupR` `instModuleR` `Fintype.card` `Pi.instFintype`	—	`Module.finrank_eq_of_rank_eq` `rank_R`
`frobenius_zmod` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `ZMod` `Semifield.toCommSemiring` `Field.toSemifield` `ZMod.instField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `RingHom.instFunLike` `frobenius` `instExpChar` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `ZMod.charP` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`induction_on` `instExpChar` `expChar_prime` `ZMod.charP` `expand_C` `frobenius_def` `C_pow` `ZMod.pow_card` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `NonUnitalAlgSemiHomClass.toMulHomClass` `expand_X`
`indicator_mem_restrictDegree` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AddMonoidAlgebra.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `restrictDegree` `Fintype.card` `indicator`	—	`mem_restrictDegree_iff_sup` `indicator.eq_1` `le_trans` `Multiset.count_le_of_le` `degrees_indicator` `le_of_eq` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_congr` `map_nsmul` `nsmul_eq_mul` `Finset.sum_eq_single` `Multiset.count_singleton` `MulZeroClass.mul_zero` `Finset.mem_univ` `Multiset.count_singleton_self` `mul_one`
`instFiniteDimensionalROfFinite` 📖	mathematical	—	`FiniteDimensional` `R` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Field.toDivisionRing` `instAddCommGroupR` `instModuleR`	—	`nonempty_fintype` `FiniteDimensional.eq_1` `IsNoetherian.iff_fg` `IsNoetherian.iff_rank_lt_aleph0` `rank_R` `Cardinal.natCast_lt_aleph0`
`ker_evalₗ` 📖	mathematical	—	`LinearMap.ker` `R` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupR` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instModuleR` `Pi.Function.module` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `evalᵢ` `Bot.bot` `Submodule` `Submodule.instBot`	—	`nonempty_fintype` `RingHomSurjective.ids` `LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank` `instFiniteDimensionalROfFinite` `FiniteDimensional.finiteDimensional_pi'` `Pi.finite` `Finite.of_fintype` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `Module.finrank_fintype_fun_eq_card` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `finrank_R` `range_evalᵢ`
`map_restrict_dom_evalₗ` 📖	mathematical	—	`Submodule.map` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.module` `Semiring.toModule` `Pi.Function.module` `RingHom.id` `RingHomSurjective.ids` `evalₗ` `restrictDegree` `Fintype.card` `Top.top` `Submodule` `Submodule.instTop`	—	`nonempty_fintype` `RingHomSurjective.ids` `top_unique` `SetLike.le_def` `instIsConcreteLE` `Submodule.mem_map` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.smul_mem` `indicator_mem_restrictDegree` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `smul_eval` `Finset.sum_eq_single` `eval_indicator_apply_eq_zero` `MulZeroClass.mul_zero` `eval_indicator_apply_eq_one` `mul_one`
`range_evalᵢ` 📖	mathematical	—	`LinearMap.range` `R` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupR` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instModuleR` `Pi.Function.module` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `evalᵢ` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `evalᵢ.eq_1` `LinearMap.range_comp` `Submodule.range_subtype` `map_restrict_dom_evalₗ`
`rank_R` 📖	mathematical	—	`Module.rank` `R` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `instAddCommGroupR` `instModuleR` `Cardinal` `Cardinal.instNatCast` `Fintype.card` `Pi.instFintype`	—	`LinearEquiv.rank_eq` `rank_finsupp_self'` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finite.of_fintype` `le_tsub_iff_right` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Fintype.card_pos_iff` `Equiv.cardinal_eq` `Cardinal.mk_fintype`

---

← Back to Index