MasonStothers

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

Statistics

Metric	Count
Definitions	0
Theorems abc	1
Total	1

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abc 📖	mathematical	IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commSemiring Semifield.toCommSemiring instAdd instZero	natDegree UniqueFactorizationMonoid.radical CommSemiring.toCommMonoidWithZero instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid commRing instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain instEuclideanDomain instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	add_eq_zero_iff_neg_eq IsCoprime.neg_right_iff mul_one IsCoprime.add_mul_left_right IsCoprime.symm add_rotate wronskian_eq_of_sum_zero IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain divRadical_dvd_wronskian_left divRadical_dvd_wronskian_right EuclideanDomain.divRadical_mul IsCoprime.mul_left IsCoprime.mul_dvd IsCoprime.divRadical IsCoprime.wronskian_eq_zero_iff mul_rotate

---

← Back to Index