SmallDegreeVieta

📁 Source: Mathlib/RingTheory/Polynomial/SmallDegreeVieta.lean

Statistics

Metric	Count
Definitions	0
Theorems aroots_quadratic_eq_pair_iff_of_ne_zero, aroots_quadratic_eq_pair_iff_of_ne_zero', eq_mul_mul_of_aroots_quadratic_eq_pair, eq_mul_mul_of_roots_quadratic_eq_pair, eq_neg_mul_add_of_aroots_quadratic_eq_pair, eq_neg_mul_add_of_roots_quadratic_eq_pair, eq_quadratic_of_degree_le_two, roots_quadratic_eq_pair_iff_of_ne_zero, roots_quadratic_eq_pair_iff_of_ne_zero'	9
Total	9

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aroots_quadratic_eq_pair_iff_of_ne_zero 📖	mathematical	—	aroots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toAdd	—	aroots_def map_add map_mul map_C map_pow map_X roots_quadratic_eq_pair_iff_of_ne_zero
aroots_quadratic_eq_pair_iff_of_ne_zero' 📖	mathematical	—	aroots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Multiset Multiset.instInsert Multiset.instSingleton Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebraMap Distrib.toMul	—	instIsDomain aroots_def map_add map_mul map_C map_pow map_X roots_quadratic_eq_pair_iff_of_ne_zero'
eq_mul_mul_of_aroots_quadratic_eq_pair 📖	mathematical	aroots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton	algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eq_mul_mul_of_roots_quadratic_eq_pair map_add map_mul map_C map_pow map_X aroots_def
eq_mul_mul_of_roots_quadratic_eq_pair 📖	mathematical	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	le_antisymm natDegree_quadratic_le Multiset.card_pair card_roots' mul_assoc coeff_add mul_coeff_zero coeff_C_zero coeff_X_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero coeff_X_zero add_zero zero_add coeff_C_mul mul_one coeff_mul_X coeff_C_succ tsub_zero Nat.instOrderedSub Even.neg_pow one_pow Multiset.esymm_pair_two coeff_eq_esymm_roots_of_card Nat.instCanonicallyOrderedAdd
eq_neg_mul_add_of_aroots_quadratic_eq_pair 📖	mathematical	aroots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton	algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toAdd	—	eq_neg_mul_add_of_roots_quadratic_eq_pair map_add map_mul map_C map_pow map_X aroots_def
eq_neg_mul_add_of_roots_quadratic_eq_pair 📖	mathematical	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toAdd	—	le_antisymm natDegree_quadratic_le Multiset.card_pair card_roots' add_comm neg_mul coeff_add coeff_C_mul coeff_X_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero coeff_mul_X coeff_C_zero zero_add coeff_C_succ add_zero mul_one pow_one mul_neg Multiset.esymm_pair_one coeff_eq_esymm_roots_of_card IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass
eq_quadratic_of_degree_le_two 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	Polynomial instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	Nat.instAtLeastTwoHAddOfNat as_sum_range_C_mul_X_pow' natDegree_le_iff_degree_le Finset.sum_range_succ Finset.sum_singleton pow_zero mul_one pow_one coeff_add coeff_C_succ coeff_mul_X add_zero coeff_C_mul coeff_X_pow zero_add coeff_C_zero Nat.instCharZero MulZeroClass.mul_zero mul_coeff_zero coeff_X_zero Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const Mathlib.Tactic.Abel.const_add_term
roots_quadratic_eq_pair_iff_of_ne_zero 📖	mathematical	—	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toAdd	—	neg_mul map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_add AddMonoidHomClass.toAddHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_gt Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat mul_ne_zero instNoZeroDivisors IsDomain.to_noZeroDivisors X_sub_C_ne_zero IsDomain.toNontrivial roots.congr_simp roots_mul roots_C roots_X_sub_C Multiset.zero_add eq_neg_mul_add_of_roots_quadratic_eq_pair eq_mul_mul_of_roots_quadratic_eq_pair
roots_quadratic_eq_pair_iff_of_ne_zero' 📖	mathematical	—	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Multiset Multiset.instInsert Multiset.instSingleton Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Distrib.toMul	—	instIsDomain roots_quadratic_eq_pair_iff_of_ne_zero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one neg_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one mul_neg one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_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.neg_congr 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 Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt

---

← Back to Index