Polynomial

📁 Source: Mathlib/NumberTheory/FLT/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems flt, flt_catalan, fermatLastTheoremWith'_polynomial	3
Total	3

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flt 📖	mathematical	IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commSemiring Semifield.toCommSemiring instAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	natDegree	—	lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_zero map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass flt_catalan LT.lt.ne' Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one mul_assoc one_ne_zero NeZero.one EuclideanDomain.toNontrivial neg_ne_zero neg_mul sub_eq_add_neg one_mul sub_eq_zero
flt_catalan 📖	mathematical	IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commSemiring Semifield.toCommSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instZero	natDegree	—	add_rotate mul_rotate

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fermatLastTheoremWith'_polynomial 📖	mathematical	—	FermatLastTheoremWith' Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commSemiring Semifield.toCommSemiring	—	FermatLastTheoremWith'.eq_1 GCDMonoid.gcd_dvd_left GCDMonoid.gcd_dvd_right gcd_ne_zero_of_left mul_add Distrib.leftDistribClass mul_pow IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain isReduced_of_noZeroDivisors Polynomial.instNoZeroDivisors Polynomial.nontrivial EuclideanDomain.toNontrivial UniqueFactorizationMonoid.normalizedFactors_pow Multiset.count_nsmul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_comm Polynomial.flt mul_ne_zero_iff EuclideanDomain.eq_div_of_mul_eq_left isCoprime_div_gcd_div_gcd mul_ne_zero mul_left_inj' Polynomial.instIsRightCancelMulZeroOfIsCancelAdd IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero pow_ne_zero Polynomial.C_ne_zero

---

← Back to Index