Spectrum

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

Statistics

Metric	Count
Definitions	0
Theorems finite_quasispectrum, finite_spectrum, 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	13
Total	13

IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_quasispectrum 📖	mathematical	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	Set.Finite quasispectrum Semifield.toCommSemiring Field.toSemifield	—	Set.encard_pair NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing Set.finite_of_encard_le_coe Set.encard_le_encard quasispectrum_subset
finite_spectrum 📖	mathematical	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set.Finite spectrum Semifield.toCommSemiring Field.toSemifield	—	Set.encard_pair NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing Set.finite_of_encard_le_coe Set.encard_le_encard spectrum_subset
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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring 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 CommRing.toCommSemiring Polynomial.eval CommSemiring.toSemiring 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 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	—	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	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	spectrum Semifield.toCommSemiring Field.toSemifield Monoid.toPow 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.toPow 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.toPow 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	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield Monoid.toPow 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