Documentation Verification Report

Three

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

Statistics

Metric	Count
Definitions `FermatLastTheoremForThreeGen`, `Solution`, `Solution'`, `a`, `b`, `c`, `multiplicity`, `u`, `Solution'_descent`, `isMinimal`, `multiplicity`, `toSolution'`	12
Theorems `H`, `coprime`, `ha`, `hb`, `hc`, `hcdvd`, `multiplicity_lambda_c_finite`, `two_le_multiplicity`, `Solution'_descent_multiplicity`, `Solution'_descent_multiplicity_lt`, `a_add_eta_mul_b`, `associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b`, `associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b`, `associated_of_dvd_a_add_eta_mul_b_of_dvd_a_add_eta_sq_mul_b`, `exists_Solution_multiplicity_lt`, `exists_minimal`, `hab`, `lambda_dvd_a_add_eta_mul_b`, `lambda_dvd_a_add_eta_sq_mul_b`, `lambda_sq_not_dvd_a_add_eta_mul_b`, `lambda_sq_not_dvd_a_add_eta_sq_mul_b`, `two_le_multiplicity`, `a_cube_add_b_cube_eq_mul`, `a_cube_b_cube_congr_one_or_neg_one`, `ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd`, `exists_Solution_of_Solution'`, `lambda_pow_four_dvd_c_cube`, `lambda_sq_dvd_c`, `lambda_sq_dvd_or_dvd_or_dvd`, `FermatLastTheoremForThree_of_FermatLastTheoremThreeGen`, `fermatLastTheoremThree`, `fermatLastTheoremThree_case_1`, `fermatLastTheoremThree_of_three_dvd_only_c`	33
Total	45

FermatLastTheoremForThreeGen

Definitions

Name	Category	Theorems
`Solution` 📖	CompData	—
`Solution'` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`a_cube_add_b_cube_eq_mul` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Solution'.a` `Solution'.b` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_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_right` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_gt` `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_pow` `Mathlib.Tactic.Ring.pow_zero` `Nat.cast_one` `IsPrimitiveRoot.toInteger_cube_eq_one` `one_mul` `IsCyclotomicExtension.Rat.Three.eta_sq` `Mathlib.Tactic.Ring.sub_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.Tactic.Ring.neg_zero` `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.isInt_add`
`a_cube_b_cube_congr_one_or_neg_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Solution'.a` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Solution'.b`	—	`NumberField.to_charZero` `Solution'.hcdvd` `IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd` `Solution'.ha` `Solution'.hb` `pow_one` `IsPrimitiveRoot.toInteger_sub_one_not_dvd_two` `Nat.fact_prime_three` `Nat.instAtLeastTwoHAddOfNat` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `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_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_bit1` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_mul` `Solution'.H` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.instAtLeastTwo`
`ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toMul` `Units.val` `Solution'.u` `Solution'.c` `IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `lambda_sq_dvd_or_dvd_or_dvd` `Solution'.H` `Solution'.coprime` `Solution'.ha` `Solution'.hb` `mul_pow` `IsPrimitiveRoot.toInteger_cube_eq_one` `one_mul` `isCoprime_mul_unit_left_right` `Units.isUnit` `mul_comm` `mul_assoc` `pow_succ'` `IsCyclotomicExtension.Rat.Three.coe_eta` `mul_one` `pow_mul` `one_pow` `IsUnit.pow` `pow_succ`
`exists_Solution_of_Solution'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`Solution.multiplicity` `Solution'.multiplicity`	—	`NumberField.to_charZero` `ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd` `Solution'.hc` `Solution'.hcdvd`
`lambda_pow_four_dvd_c_cube` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Solution'.c`	—	`NumberField.to_charZero` `a_cube_b_cube_congr_one_or_neg_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.pow_add` `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_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Solution'.H` `Units.inv_mul_cancel_left`
`lambda_sq_dvd_c` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Solution'.c`	—	`NumberField.to_charZero` `Solution'.multiplicity_lambda_c_finite` `lambda_pow_four_dvd_c_cube` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `FiniteMultiplicity.emultiplicity_eq_multiplicity` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `emultiplicity_pow` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `IsPrimitiveRoot.zeta_sub_one_prime'` `pow_dvd_iff_le_emultiplicity` `pow_multiplicity_dvd` `mul_assoc` `pow_add` `add_tsub_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub`
`lambda_sq_dvd_or_dvd_or_dvd` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Solution'.a` `Solution'.b` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `finiteMultiplicity_iff_emultiplicity_ne_top` `Nat.instAtLeastTwoHAddOfNat` `emultiplicity_lt_iff_not_dvd` `IsCyclotomicExtension.Rat.Three.coe_eta` `Dvd.dvd.mul_left` `pow_dvd_pow_of_dvd` `lambda_sq_dvd_c` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `FiniteMultiplicity.emultiplicity_eq_multiplicity` `Nat.cast_le` `Nat.cast_add` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `emultiplicity_mul` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `IsPrimitiveRoot.zeta_sub_one_prime'` `pow_dvd_iff_le_emultiplicity` `a_cube_add_b_cube_eq_mul` `Solution'.H` `pow_mul`

FermatLastTheoremForThreeGen.Solution

Definitions

Name	Category	Theorems
`Solution'_descent` 📖	CompOp	2 math math: `Solution'_descent_multiplicity_lt`, `Solution'_descent_multiplicity`
`isMinimal` 📖	MathDef	1 math math: `exists_minimal`
`multiplicity` 📖	CompOp	5 math math: `FermatLastTheoremForThreeGen.exists_Solution_of_Solution'`, `exists_Solution_multiplicity_lt`, `Solution'_descent_multiplicity_lt`, `two_le_multiplicity`, `Solution'_descent_multiplicity`
`toSolution'` 📖	CompOp	6 math math: `lambda_sq_not_dvd_a_add_eta_sq_mul_b`, `lambda_dvd_a_add_eta_sq_mul_b`, `hab`, `a_add_eta_mul_b`, `lambda_sq_not_dvd_a_add_eta_mul_b`, `lambda_dvd_a_add_eta_mul_b`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Solution'_descent_multiplicity` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`FermatLastTheoremForThreeGen.Solution'.multiplicity` `Solution'_descent` `multiplicity`	—	`NumberField.to_charZero` `multiplicity_eq_of_dvd_of_not_dvd` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `NumberField.RingOfIntegers.instNontrivial` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `Prime.ne_zero` `IsPrimitiveRoot.zeta_sub_one_prime'` `mul_assoc` `pow_succ`
`Solution'_descent_multiplicity_lt` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`FermatLastTheoremForThreeGen.Solution'.multiplicity` `Solution'_descent` `multiplicity`	—	`NumberField.to_charZero` `Solution'_descent_multiplicity` `two_le_multiplicity`
`a_add_eta_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `FermatLastTheoremForThreeGen.Solution'.b` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `IsCyclotomicExtension.Rat.Three.coe_eta` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `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`
`associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing` `Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `FermatLastTheoremForThreeGen.Solution'.b` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `NumberField.RingOfIntegers.instIsDomain` `IsCyclotomicExtension.Rat.three_pid` `dvd_mul_sub_mul_mul_gcd_of_dvd` `one_mul` `IsUnit.dvd_mul_right` `gcd_isUnit_iff` `IsBezout.of_isPrincipalIdealRing` `FermatLastTheoremForThreeGen.Solution'.coprime` `IsCyclotomicExtension.Rat.Three.coe_eta` `Prime.associated_of_dvd` `IsDomain.toIsCancelMulZero` `IsPrimitiveRoot.zeta_sub_one_prime'` `Nat.fact_prime_three`
`associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing` `Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `FermatLastTheoremForThreeGen.Solution'.b` `Distrib.toMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	`Associated` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `NumberField.RingOfIntegers.instIsDomain` `IsCyclotomicExtension.Rat.three_pid` `dvd_mul_sub_mul_mul_gcd_of_dvd` `one_mul` `IsCyclotomicExtension.Rat.Three.eta_sq` `neg_sub` `sub_mul` `neg_mul` `pow_two` `IsCyclotomicExtension.Rat.Three.coe_eta` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `dvd_mul_of_dvd_left` `dvd_neg` `IsUnit.dvd_mul_right` `gcd_isUnit_iff` `IsBezout.of_isPrincipalIdealRing` `FermatLastTheoremForThreeGen.Solution'.coprime` `mul_one` `Prime.associated_of_dvd` `IsDomain.toIsCancelMulZero` `IsPrimitiveRoot.zeta_sub_one_prime'` `Nat.fact_prime_three`
`associated_of_dvd_a_add_eta_mul_b_of_dvd_a_add_eta_sq_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing` `Prime` `NumberField.RingOfIntegers` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `FermatLastTheoremForThreeGen.Solution'.b` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Associated` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `NumberField.RingOfIntegers.instIsDomain` `IsCyclotomicExtension.Rat.three_pid` `dvd_mul_sub_mul_mul_gcd_of_dvd` `one_mul` `Nat.instAtLeastTwoHAddOfNat` `IsCyclotomicExtension.Rat.Three.eta_sq` `mul_assoc` `pow_two` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.pow_congr` `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.mul_one` `IsCyclotomicExtension.Rat.Three.coe_eta` `dvd_mul_of_dvd_left` `IsUnit.dvd_mul_right` `gcd_isUnit_iff` `IsBezout.of_isPrincipalIdealRing` `FermatLastTheoremForThreeGen.Solution'.coprime` `mul_one` `Prime.associated_of_dvd` `IsDomain.toIsCancelMulZero` `IsPrimitiveRoot.zeta_sub_one_prime'` `Nat.fact_prime_three`
`exists_Solution_multiplicity_lt` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`multiplicity`	—	`NumberField.to_charZero` `FermatLastTheoremForThreeGen.exists_Solution_of_Solution'` `Solution'_descent_multiplicity_lt`
`exists_minimal` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`isMinimal`	—	`Nat.find_spec` `Nat.find_min'`
`hab` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `FermatLastTheoremForThreeGen.Solution'.b`	—	—
`lambda_dvd_a_add_eta_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `FermatLastTheoremForThreeGen.Solution'.b`	—	`dvd_add` `Distrib.leftDistribClass` `dvd_trans` `dvd_pow_self` `hab` `mul_comm` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `a_add_eta_mul_b`
`lambda_dvd_a_add_eta_sq_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `Distrib.toMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `FermatLastTheoremForThreeGen.Solution'.b`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `Nat.instAtLeastTwoHAddOfNat` `IsCyclotomicExtension.Rat.Three.coe_eta` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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_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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `dvd_add` `Distrib.leftDistribClass` `dvd_trans` `dvd_pow_self` `hab`
`lambda_sq_not_dvd_a_add_eta_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `FermatLastTheoremForThreeGen.Solution'.b`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `a_add_eta_mul_b` `dvd_add_right` `hab` `pow_two` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `Prime.ne_zero` `IsPrimitiveRoot.zeta_sub_one_prime'` `FermatLastTheoremForThreeGen.Solution'.hb`
`lambda_sq_not_dvd_a_add_eta_sq_mul_b` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `FermatLastTheoremForThreeGen.Solution'.a` `toSolution'` `Distrib.toMul` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `FermatLastTheoremForThreeGen.Solution'.b`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `hab` `FermatLastTheoremForThreeGen.Solution'.hb` `sub_eq_iff_eq_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `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.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `IsCyclotomicExtension.Rat.Three.eta_sq` `Mathlib.Tactic.Ring.one_mul` `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.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` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `Prime.ne_zero` `IsPrimitiveRoot.zeta_sub_one_prime'` `mul_assoc` `pow_two` `IsCyclotomicExtension.Rat.Three.coe_eta` `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`
`two_le_multiplicity` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`multiplicity`	—	`NumberField.to_charZero` `FermatLastTheoremForThreeGen.Solution'.two_le_multiplicity`

FermatLastTheoremForThreeGen.Solution'

Definitions

Name	Category	Theorems
`a` 📖	CompOp	12 math math: `FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b`, `FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b`, `H`, `FermatLastTheoremForThreeGen.Solution.hab`, `FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b`, `ha`, `FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one`, `coprime`, `FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul`, `FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b`, `FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b`, `FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd`
`b` 📖	CompOp	12 math math: `FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b`, `FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b`, `H`, `FermatLastTheoremForThreeGen.Solution.hab`, `FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b`, `FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one`, `hb`, `coprime`, `FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul`, `FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b`, `FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b`, `FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd`
`c` 📖	CompOp	6 math math: `FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube`, `H`, `hcdvd`, `FermatLastTheoremForThreeGen.lambda_sq_dvd_c`, `multiplicity_lambda_c_finite`, `FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd`
`multiplicity` 📖	CompOp	4 math math: `FermatLastTheoremForThreeGen.exists_Solution_of_Solution'`, `FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity_lt`, `two_le_multiplicity`, `FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity`
`u` 📖	CompOp	2 math math: `H`, `FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`H` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `a` `b` `Distrib.toMul` `Units.val` `u` `c`	—	—
`coprime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`IsCoprime` `NumberField.RingOfIntegers` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `a` `b`	—	—
`ha` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `a`	—	—
`hb` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `b`	—	—
`hc` 📖	—	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	—	—	—
`hcdvd` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `c`	—	—
`multiplicity_lambda_c_finite` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`FiniteMultiplicity` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `c`	—	`NumberField.to_charZero` `FiniteMultiplicity.of_not_isUnit` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `IsNoetherianRing.wfDvdMonoid` `NumberField.RingOfIntegers.extension_isNoetherian` `Prime.not_unit` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `IsPrimitiveRoot.zeta_sub_one_prime'` `hc`
`two_le_multiplicity` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing`	`multiplicity`	—	`NumberField.to_charZero` `FiniteMultiplicity.le_multiplicity_of_pow_dvd` `multiplicity_lambda_c_finite` `FermatLastTheoremForThreeGen.lambda_sq_dvd_c`

(root)

Definitions

Name	Category	Theorems
`FermatLastTheoremForThreeGen` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FermatLastTheoremForThree_of_FermatLastTheoremThreeGen` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Field.toCommRing` `FermatLastTheoremForThreeGen`	`FermatLastTheoremFor`	—	`NumberField.to_charZero` `fermatLastTheoremThree_of_three_dvd_only_c` `NumberField.RingOfIntegers.instCharZero_1` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two'` `Ideal.norm_dvd_iff` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two'` `dvd_trans` `IsPrimitiveRoot.toInteger_sub_one_dvd_prime'` `Nat.instAtLeastTwoHAddOfNat` `Int.cast_mul` `Int.cast_ofNat` `eq_intCast` `RingHom.instRingHomClass` `IsCoprime.map` `one_mul`
`fermatLastTheoremThree` 📖	mathematical	—	`FermatLastTheoremFor`	—	`CyclotomicField.instCharZero` `Rat.instCharZero` `CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero` `IsCyclotomicExtension.zeta_spec` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `FermatLastTheoremForThree_of_FermatLastTheoremThreeGen` `FermatLastTheoremForThreeGen.exists_Solution_of_Solution'` `FermatLastTheoremForThreeGen.Solution.exists_minimal` `FermatLastTheoremForThreeGen.Solution.exists_Solution_multiplicity_lt` `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` `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.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing`
`fermatLastTheoremThree_case_1` 📖	—	—	—	—	`Int.cast_add` `Int.cast_pow` `Nat.instAtLeastTwoHAddOfNat` `Prime.dvd_mul` `Int.prime_three`
`fermatLastTheoremThree_of_three_dvd_only_c` 📖	mathematical	—	`FermatLastTheoremFor`	—	`fermatLastTheoremFor_iff_int` `fermatLastTheoremWith_of_fermatLastTheoremWith_coprime` `Int.instIsDomain` `Prime.dvd_mul` `Int.prime_three` `Finset.gcd_insert` `Finset.gcd_singleton` `abs_neg` `Odd.neg_pow` `sub_eq_add_neg` `sub_eq_zero` `Finset.insert_comm` `add_comm` `neg_ne_zero` `Finset.pair_comm` `add_assoc` `fermatLastTheoremThree_case_1`

---

← Back to Index