ConjRootClass

📁 Source: Mathlib/FieldTheory/Minpoly/ConjRootClass.lean

Statistics

Metric	Count
Definitions ConjRootClass, carrier, instDecidableEqOfNormalOfFintypeAlgEquiv, instDecidablePredMemSetCarrierOfNormalOfDecidableEqOfFintypeAlgEquiv, instFintypeElemCarrierOfNormalOfDecidableEqOfAlgEquiv, instInvolutiveNeg, instNeg, instZero, minpoly, mk	10
Theorems aeval_minpoly_iff, aroots_minpoly_eq_carrier_val, carrier_eq_mk_aroots_minpoly, carrier_inj, carrier_neg, carrier_zero, exists_mem_carrier_add_eq_zero, ind, irreducible_minpoly, mem_carrier, map_eq_prod, minpoly_inj, minpoly_injective, minpoly_mk, minpoly_ne_zero, mk_def, mk_eq_mk, mk_eq_zero_iff, mk_neg, mk_zero, monic_minpoly, nodup_aroots_minpoly, rootSet_minpoly_eq_carrier, separable_minpoly, splits_minpoly	25
Total	35

ConjRootClass

Definitions

Name	Category	Theorems
carrier 📖	CompOp	9 math math: rootSet_minpoly_eq_carrier, minpoly.map_eq_prod, carrier_zero, carrier_inj, exists_mem_carrier_add_eq_zero, aroots_minpoly_eq_carrier_val, carrier_eq_mk_aroots_minpoly, mem_carrier, carrier_neg
instDecidableEqOfNormalOfFintypeAlgEquiv 📖	CompOp	—
instDecidablePredMemSetCarrierOfNormalOfDecidableEqOfFintypeAlgEquiv 📖	CompOp	—
instFintypeElemCarrierOfNormalOfDecidableEqOfAlgEquiv 📖	CompOp	—
instInvolutiveNeg 📖	CompOp	—
instNeg 📖	CompOp	3 math math: mk_neg, exists_mem_carrier_add_eq_zero, carrier_neg
instZero 📖	CompOp	3 math math: mk_zero, carrier_zero, mk_eq_zero_iff
minpoly 📖	CompOp	13 math math: minpoly_inj, aeval_minpoly_iff, separable_minpoly, rootSet_minpoly_eq_carrier, minpoly.map_eq_prod, minpoly_injective, monic_minpoly, minpoly_mk, splits_minpoly, nodup_aroots_minpoly, aroots_minpoly_eq_carrier_val, carrier_eq_mk_aroots_minpoly, irreducible_minpoly
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_minpoly_iff 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	ind isConjRoot_iff_aeval_eq_zero Algebra.IsIntegral.isIntegral instIsDomain Algebra.IsAlgebraic.isIntegral comm IsEquiv.toSymm IsConjRoot.instIsEquiv
aroots_minpoly_eq_carrier_val 📖	mathematical	—	Polynomial.aroots EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly instIsDomain Field.toSemifield Finset.val Set.toFinset carrier	—	instIsDomain Set.toFinset_congr Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.rootSet_def Finset.toFinset_coe Multiset.Nodup.dedup nodup_aroots_minpoly
carrier_eq_mk_aroots_minpoly 📖	mathematical	—	Set.toFinset carrier Polynomial.aroots EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly instIsDomain Field.toSemifield nodup_aroots_minpoly	—	instIsDomain nodup_aroots_minpoly aroots_minpoly_eq_carrier_val
carrier_inj 📖	mathematical	—	ConjRootClass Set carrier	—	ind
carrier_neg 📖	mathematical	—	carrier ConjRootClass instNeg Set InvolutiveNeg.toNeg Set.involutiveNeg HasDistribNeg.toInvolutiveNeg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NonUnitalNonAssocRing.toHasDistribNeg	—	Set.ext
carrier_zero 📖	mathematical	—	carrier ConjRootClass instZero Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Set.ext mem_carrier mk_eq_zero_iff Set.mem_singleton_iff
exists_mem_carrier_add_eq_zero 📖	mathematical	—	Set Set.instMembership carrier Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass ConjRootClass instNeg	—	mk_neg add_eq_zero_iff_eq_neg IsConjRoot.refl ind neg_add_cancel
ind 📖	—	—	—	—	—
irreducible_minpoly 📖	mathematical	—	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring minpoly	—	ind minpoly.irreducible instIsDomain Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral
mem_carrier 📖	mathematical	—	Set Set.instMembership carrier	—	—
minpoly_inj 📖	mathematical	—	minpoly	—	ind
minpoly_injective 📖	mathematical	—	ConjRootClass Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield minpoly	—	—
minpoly_mk 📖	mathematical	—	minpoly minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	—
minpoly_ne_zero 📖	—	—	—	—	Polynomial.Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing monic_minpoly
mk_def 📖	mathematical	—	IsConjRoot.setoid EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	—
mk_eq_mk 📖	mathematical	—	IsConjRoot EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	Quotient.eq
mk_eq_zero_iff 📖	mathematical	—	ConjRootClass instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	mk_zero isConjRoot_zero_iff_eq_zero instIsDomain
mk_neg 📖	mathematical	—	ConjRootClass instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	—
mk_zero 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain ConjRootClass instZero	—	—
monic_minpoly 📖	mathematical	—	Polynomial.Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield minpoly	—	ind minpoly.monic Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral
nodup_aroots_minpoly 📖	mathematical	—	Multiset.Nodup Polynomial.aroots EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly instIsDomain Field.toSemifield	—	Polynomial.nodup_roots instIsDomain Polynomial.Separable.map separable_minpoly
rootSet_minpoly_eq_carrier 📖	mathematical	—	Polynomial.rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly instIsDomain Field.toSemifield carrier	—	Set.ext instIsDomain mem_carrier Polynomial.mem_rootSet instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors aeval_minpoly_iff minpoly_ne_zero
separable_minpoly 📖	mathematical	—	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield minpoly	—	ind Algebra.IsSeparable.isSeparable
splits_minpoly 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly	—	ind Normal.splits

ConjRootClass.minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_prod 📖	mathematical	—	Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebraMap ConjRootClass.minpoly Finset.prod Polynomial CommRing.toCommMonoid Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Set.toFinset ConjRootClass.carrier Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	instIsDomain Finset.prod_congr Set.toFinset_congr Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing Multiset.map_congr Polynomial.rootSet_def Finset.toFinset_coe Multiset.dedup_eq_self Polynomial.nodup_roots Polynomial.Separable.map ConjRootClass.separable_minpoly Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq Polynomial.Monic.map ConjRootClass.monic_minpoly Polynomial.splits_iff_card_roots ConjRootClass.splits_minpoly

(root)

Definitions

Name	Category	Theorems
ConjRootClass 📖	CompOp	8 math math: ConjRootClass.mk_zero, ConjRootClass.minpoly_injective, ConjRootClass.carrier_zero, ConjRootClass.carrier_inj, ConjRootClass.mk_neg, ConjRootClass.mk_eq_zero_iff, ConjRootClass.exists_mem_carrier_add_eq_zero, ConjRootClass.carrier_neg

---

← Back to Index