Disc

📁 Source: Mathlib/LinearAlgebra/Matrix/Charpoly/Disc.lean

Statistics

Metric	Count
Definitions disc, discr	2
Theorems disc_fin_two, disc_of_card_eq_two, discr_fin_two, discr_of_card_eq_two	4
Total	6

Matrix

Definitions

Name	Category	Theorems
disc 📖	CompOp	—
discr 📖	CompOp	10 math math: discr_conj, discr_of_card_eq_two, sub_scalar_sq_eq_disc, disc_fin_two, discr_conj', disc_conj, disc_of_card_eq_two, disc_conj', sub_scalar_sq_eq_discr, discr_fin_two

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disc_fin_two 📖	mathematical	—	discr Fin.fintype SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat det	—	discr_fin_two
disc_of_card_eq_two 📖	mathematical	Fintype.card	discr SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat det	—	discr_of_card_eq_two
discr_fin_two 📖	mathematical	—	discr Fin.fintype SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat det	—	discr_of_card_eq_two Fintype.card_fin
discr_of_card_eq_two 📖	mathematical	Fintype.card	discr SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat det	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nat.instAtLeastTwoHAddOfNat discr.eq_1 Polynomial.discr_of_degree_eq_two charpoly_degree_eq_dim WithBot.charZero Nat.instCharZero charpoly_of_card_eq_two Polynomial.coeff_add Polynomial.coeff_sub Polynomial.coeff_X_pow Polynomial.coeff_mul_X Polynomial.coeff_C_zero zero_sub Polynomial.coeff_C_succ add_zero Even.neg_pow Polynomial.mul_coeff_zero Polynomial.coeff_X_zero MulZeroClass.mul_zero sub_self zero_add sub_zero mul_one

---

← Back to Index