QuadraticDiscriminant

📁 Source: Mathlib/Algebra/QuadraticDiscriminant.lean

Statistics

Metric	Count
Definitions discrim	1
Theorems discrim_eq_sq_of_quadratic_eq_zero, discrim_eq_zero_iff, discrim_eq_zero_of_existsUnique, discrim_le_zero, discrim_le_zero_of_nonpos, discrim_lt_zero, discrim_lt_zero_of_neg, discrim_neg, exists_quadratic_eq_zero, quadratic_eq_zero_iff, quadratic_eq_zero_iff_discrim_eq_sq, quadratic_eq_zero_iff_of_discrim_eq_zero, quadratic_ne_zero_of_discrim_ne_sq	13
Total	14

(root)

Definitions

Name	Category	Theorems
discrim 📖	CompOp	9 math math: discrim_le_zero_of_nonpos, discrim_eq_zero_iff, discrim_le_zero, discrim_eq_zero_of_existsUnique, quadratic_eq_zero_iff_discrim_eq_sq, discrim_eq_sq_of_quadratic_eq_zero, discrim_lt_zero, discrim_lt_zero_of_neg, discrim_neg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrim_eq_sq_of_quadratic_eq_zero 📖	mathematical	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	discrim CommRing.toRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat discrim.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf 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_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf 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
discrim_eq_zero_iff 📖	mathematical	—	discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing ExistsUnique Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat quadratic_eq_zero_iff_of_discrim_eq_zero discrim_eq_zero_of_existsUnique
discrim_eq_zero_of_existsUnique 📖	mathematical	ExistsUnique Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Nat.instAtLeastTwoHAddOfNat quadratic_eq_zero_iff_discrim_eq_sq IsDomain.to_noZeroDivisors Field.isDomain
discrim_le_zero 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	discrim.eq_1 sq lt_trichotomy Filter.tendsto_atBot_add_const_right IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Filter.Tendsto.atBot_mul_atTop₀ Filter.Tendsto.const_mul_atTop_of_neg Filter.tendsto_id Filter.Eventually.exists Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Filter.Tendsto.eventually Filter.eventually_lt_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial LE.le.not_gt mul_assoc add_mul Distrib.rightDistribClass eq_or_ne MulZeroClass.mul_zero MulZeroClass.zero_mul sub_self instReflLe le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add 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.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.without_one_mul Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.CancelDenoms.add_subst Mathlib.Tactic.CancelDenoms.mul_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.CancelDenoms.neg_subst Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_div_cancel₀ Nat.instAtLeastTwoHAddOfNat mul_nonneg IsOrderedRing.toPosMulMono zero_le_four IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono LT.lt.le Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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'_ofNat Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.FieldSimp.subst_add neg_div neg_mul_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval mul_neg ne_of_gt Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 neg_nonpos
discrim_le_zero_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	discrim_le_zero discrim_neg neg_mul IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
discrim_lt_zero 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	le_of_lt lt_of_le_of_ne discrim_le_zero Nat.instAtLeastTwoHAddOfNat mul_assoc quadratic_eq_zero_iff_of_discrim_eq_zero ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_congr 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.without_one_mul Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.CancelDenoms.add_subst Mathlib.Tactic.CancelDenoms.mul_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.sub_neg_of_lt sub_eq_zero_of_eq
discrim_lt_zero_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	discrim_lt_zero neg_ne_zero discrim_neg neg_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
discrim_neg 📖	mathematical	—	discrim NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Even.neg_pow Nat.instAtLeastTwoHAddOfNat mul_neg neg_mul neg_neg
exists_quadratic_eq_zero 📖	mathematical	discrim DivisionRing.toRing Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instAtLeastTwoHAddOfNat quadratic_eq_zero_iff
quadratic_eq_zero_iff 📖	mathematical	discrim DivisionRing.toRing Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	Nat.instAtLeastTwoHAddOfNat quadratic_eq_zero_iff_discrim_eq_sq IsDomain.to_noZeroDivisors Field.isDomain sq mul_self_eq_mul_self_iff 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 Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg 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 Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.subst_sub
quadratic_eq_zero_iff_discrim_eq_sq 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass discrim CommRing.toRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat discrim_eq_sq_of_quadratic_eq_zero mul_ne_zero mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero NoZeroDivisors.to_isCancelMulZero Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd discrim.eq_1 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf 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.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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf
quadratic_eq_zero_iff_of_discrim_eq_zero 📖	mathematical	discrim DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero quadratic_eq_zero_iff add_zero sub_zero
quadratic_ne_zero_of_discrim_ne_sq 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat discrim_eq_sq_of_quadratic_eq_zero

---

← Back to Index