Documentation Verification Report

Spectrum

📁 Source: Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

Statistics

Metric	Count
Definitions	0
Theorems `quasispectrum_subset`, `spectrum_subset`, `exists_mem_of_not_isUnit_aeval_prod`, `map_polynomial_aeval_of_degree_pos`, `map_polynomial_aeval_of_nonempty`, `map_pow_of_nonempty`, `map_pow_of_pos`, `nonempty_of_isAlgClosed_of_finiteDimensional`, `pow_image_subset`, `pow_mem_pow`, `subset_polynomial_aeval`	11
Total	11

IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasispectrum_subset` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`Set` `Set.instHasSubset` `quasispectrum` `Semifield.toCommSemiring` `Field.toSemifield` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set.instSingletonSet` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`IsScalarTower.left` `spectrum_subset` `Unitization.IsIdempotentElem.inr` `Unitization.quasispectrum_eq_spectrum_inr'`
`spectrum_subset` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Set` `Set.instHasSubset` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set.instSingletonSet` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `spectrum.of_subsingleton` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_subset_iff` `spectrum.subset_polynomial_aeval` `eq_zero_or_one_of_sq_eq_self` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Polynomial.eval_sub` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.aeval_sub` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `pow_two` `eq` `sub_self` `spectrum.zero_eq`

spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_of_not_isUnit_aeval_prod` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Multiset.prod` `CommRing.toCommMonoid` `Polynomial.commRing` `Multiset.map` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.roots`	`Set` `Set.instMembership` `spectrum` `Polynomial.eval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`List.prod_isUnit` `map_list_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Multiset.prod_toList` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Polynomial.aeval_X` `Polynomial.aeval_C` `mem_iff` `IsUnit.sub_iff` `Polynomial.mem_roots'`
`map_polynomial_aeval_of_degree_pos` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Polynomial.degree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`spectrum` `Semifield.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Set.image` `Polynomial.eval`	—	`Set.eq_of_subset_of_subset` `instIsDomain` `Polynomial.Splits.eq_prod_roots` `IsAlgClosed.splits` `Polynomial.ne_zero_of_degree_gt` `Polynomial.degree_sub_eq_right_of_degree_lt` `lt_of_le_of_lt` `Polynomial.degree_C_le` `Polynomial.leadingCoeff_ne_zero` `Units.isUnit` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_C` `exists_mem_of_not_isUnit_aeval_prod` `Commute.isUnit_mul_iff` `Commute.map` `NonUnitalAlgSemiHomClass.toMulHomClass` `Commute.all` `Polynomial.aeval_mul` `mem_iff` `symm` `IsEquiv.toSymm` `eq_isEquiv` `Polynomial.eval_sub` `Polynomial.eval_C` `subset_polynomial_aeval`
`map_polynomial_aeval_of_nonempty` 📖	mathematical	`Set.Nonempty` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield`	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Set.image` `Polynomial.eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `of_subsingleton` `Set.image_empty` `le_or_gt` `Polynomial.eq_C_of_degree_le_zero` `Polynomial.aeval_C` `scalar_eq` `Set.image_congr` `Polynomial.eval_C` `Set.Nonempty.image_const` `map_polynomial_aeval_of_degree_pos`
`map_pow_of_nonempty` 📖	mathematical	`Set.Nonempty` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Set.image` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Polynomial.aeval_X_pow` `Set.image_congr` `Polynomial.eval_X_pow` `map_polynomial_aeval_of_nonempty`
`map_pow_of_pos` 📖	mathematical	—	`spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Set.image` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Polynomial.aeval_X_pow` `Set.image_congr` `Polynomial.eval_X_pow` `map_polynomial_aeval_of_degree_pos` `Polynomial.degree_X_pow` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `Nat.cast_pos` `WithBot.instIsOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `WithBot.nontrivial`
`nonempty_of_isAlgClosed_of_finiteDimensional` 📖	mathematical	—	`Set.Nonempty` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield`	—	`isIntegral_of_noetherian` `IsNoetherian.iff_fg` `Polynomial.aeval_def` `NeZero.one` `exists_mem_of_not_isUnit_aeval_prod` `instIsDomain` `Polynomial.Splits.eq_prod_roots_of_monic` `IsAlgClosed.splits`
`pow_image_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `spectrum` `Semifield.toCommSemiring` `Ring.toSemiring`	—	`Set.image_congr` `Polynomial.eval_X_pow` `Polynomial.aeval_X_pow` `subset_polynomial_aeval`
`pow_mem_pow` 📖	mathematical	`Set` `Set.instMembership` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`pow_image_subset`
`subset_polynomial_aeval` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.image` `Polynomial.eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `spectrum` `Semifield.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval`	—	`Polynomial.eval_sub` `Polynomial.eval_C` `sub_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_C` `mem_iff` `neg_sub` `neg_mul_neg` `Polynomial.mul_div_eq_iff_isRoot` `Polynomial.aeval_mul` `Commute.map` `NonUnitalAlgSemiHomClass.toMulHomClass` `Commute.all` `Commute.isUnit_mul_iff` `Polynomial.aeval_X`

---

← Back to Index