Trust
Axioms come from the Lean kernel (Lean (version 4.35.0-rc3, x86_64-w64-windows-gnu, commit 470d5ce1400764999581fd26d5d72b00d990b0f4, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.
Lake environment and dependency-pin digest: 29cfd5efd9ef7c84.
Verification scope: all declaration-bearing files; 243 of 243 eligible files selected, 3139 declarations requested.
Rendering mode: clean content-bound cache results only; 0 selected files had no reusable result and remain UNKNOWN. No Lean process was started for those misses during this static-site build.
Per-file probe bounds: 300 seconds. A resource stop is UNKNOWN, never a failed proof.
- no axioms
- 76
- standard axioms
- 2586
- sorry
- 90
- extra axioms
- 49
- unknown
- 338
What the badges mean
- no axioms
- Lean's kernel checked the proof, and it rests on nothing but Lean's rules.
- standard axioms
- Checked by the kernel, using only propext, Classical.choice or Quot.sound: the three axioms nearly all of mathematics in Lean uses.
- extra axioms
- Checked by the kernel, but it assumes something the project declared with `axiom`. It is only as true as those assumptions.
- depends on sorry
- Not proved: somewhere in it, or in something it uses, a proof was left out (`sorry`).
- trust unknown
- Lean did not check it: Lean was not run, the file did not elaborate, or Lean has no constant by that name.
Files where Lean reported errors
FLT/Data/QHat.lean: line 722: Tactic `rcases` failed: `h : ∀ t ∈ Set.range fun S => ⋂ (_ : S ∈ {x | unitsratsub ≤ x ∧ unitszHatsub ≤ x}), ↑S, (2 total)FLT/DedekindDomain/Completion/BaseChange.lean: line 580: Tactic `rfl` failed: The left-hand side (1 total)FLT/DivisionAlgebra/Finiteness.lean: line 565: Tactic `rewrite` failed: Did not find an occurrence of the pattern (10 total)FLT/HenselianLocalRing/Finite.lean: line 290: unsolved goals (1 total)
Trust UNKNOWN declarations (338)
TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.IsDedekindDomain.FiniteAdeleRing.toAdicCompletion_applyFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStructFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mem_formFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.smul_le_smul_iffFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.inv_smul_le_iffFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.smul_infFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.QuotientGroup.exists_bijOn_mk_image_mul_singletonFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra._root_.Polynomial.cyclotomic_of_charPFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalar_auxFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.le_inv_smul_iffFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.le_smul_supFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.smul_supFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.HeckeAlgebra._root_.Algebra.coe_adjoin_inductionFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.HeckeAlgebra._root_.DirectSum.IsInternal.reindexFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean trust unknown: Lean has no constant by this nameTotallyDefiniteQuaternionAlgebra.HeckeAlgebra._root_.AlgHom.map_zeroFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean trust unknown: Lean has no constant by this nameHurwitz.auxFLT/Data/Hurwitz.lean trust unknown: Lean has no constant by this nameHurwitz.aux2FLT/Data/Hurwitz.lean trust unknown: Lean has no constant by this nameZHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.toZModFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.toZMod_defFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.propFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.extFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.zero_valFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.one_valFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.ofNat_valFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.natCast_valFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.intCast_valFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.commRingFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.zeroNeOneFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.nontrivialFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.charZeroFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.eFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.e_defFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat._root_.Nat.sum_factorial_lt_factorial_succFLT/Data/QHat.lean trust unknown: Lean has no constant by this nameZHat._root_.Nat.sum_factorial_lt_two_mul_factorialFLT/Data/QHat.lean trust unknown: Lean has no constant by this nameZHat.e_factorial_succFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.e_not_in_IntFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.torsionfree_auxFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.nat_mul_applyFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.pnat_mul_applyFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.eq_zero_of_mul_eq_zeroFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.torsionfreeFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.ZHat_flatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.y_mul_N_eq_zFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.multiplesFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileZHat.nat_denseFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.canonicalFormFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.IsCoprimeFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.isUnit_iff_coprimeFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.isCoprime_iff_coprimeFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.i₂FLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.injective_zHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.nontrivial_QHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.i₁FLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.injective_ratFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.PNat.lcm_commFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.lowestTermsFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.ratsubFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.zHatsubFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.zsubFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.ZMod.isUnit_natAbsFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat._root_.Algebra.TensorProduct.one_tmul_intCastFLT/Data/QHat.lean trust unknown: Lean has no constant by this nameQHat.rat_meet_zHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.rat_join_zHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.unitsratsubFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.unitszHatsubFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.unitszsubFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat.unitsrat_meet_unitszHatFLT/Data/QHat.lean trust unknown: Lean reported 2 error(s) in this fileQHat._root_.Algebra.TensorProduct.intCast_tmul_oneFLT/Data/QHat.lean trust unknown: Lean has no constant by this nameQHat._root_.Algebra.TensorProduct.one_tmul_natCastFLT/Data/QHat.lean trust unknown: Lean has no constant by this nameIsDedekindDomain.HeightOneSpectrum.adicValued.continuous_algebraMapFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension._root_.WithVal.semialgebraMapFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean has no constant by this nameIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHomFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_coeFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_continuousFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHomFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegersFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPiFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_tmul_applyFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRightFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_surjectiveFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPiFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_isOpenQuotientMapFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_tmulFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_range_subset_closureFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_isClopen_rangeFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.range_tensorAdicCompletionIntegersTo_eq_closure_range_algebraMapFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.pi_adicCompletionIntegers_eq_closure_range_algebraMapFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.isClosed_baseChange_image_closure_range_algebraMapFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_piFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionIntegersRingHomFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.Extension.integer_algebraMap_applyFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion._root_.WithZero.ofAdd_neg_ofNat_powFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean has no constant by this nameIsDedekindDomain.HeightOneSpectrum.adicCompletion.liesOver_completionIdealFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_eq_ramificationIdxFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.inertiaDeg_eq_inertiaDegFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmoduleFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoeFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe_tmulFLT/DedekindDomain/Completion/BaseChange.lean trust unknown: Lean reported 1 error(s) in this fileIsDedekindDomain.HeightOneSpectrum._root_.Ideal.sum_ramification_inertia_extensionsFLT/DedekindDomain/IntegralClosure.lean trust unknown: Lean has no constant by this name_root_.IsIntegralClosure.isLocalizedModuleFLT/DedekindDomain/IntegralClosure.lean trust unknown: Lean has no constant by this nameDeformation.ProartinianCat._root_.CategoryTheory.Iso.toContinuousAlgEquivFLT/Deformations/Categories.lean trust unknown: Lean has no constant by this nameIsArithFrobAt._root_.arithFrobAt'FLT/Deformations/RepresentationTheory/Frobenius.lean trust unknown: Lean has no constant by this nameIsArithFrobAt._root_.isConj_arithFrobAt'FLT/Deformations/RepresentationTheory/Frobenius.lean trust unknown: Lean has no constant by this nameNumberField.AdeleRing.DivisionAlgebra.Aux.DfFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.DfxFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.DinfFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.DinfxFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.inclFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.incl₁FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.inclKn𝔸KnFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.Kn_discreteFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.DIsoFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸IsoFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸IsoTopFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete_auxFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D_discreteFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.includeLeftSubgroupFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.discrete_includeLeft_subgroupFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.discrete_principalSubgroupFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.compact_includeLeft_subgroupFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.not_injective_of_large_measureFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight'FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight''FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightUnitsFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.smul_D𝔸_prodRight_symmFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units_contFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjectiveFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_auxFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.InfiniteAdeleRing.realToCompletionFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.InfiniteAdeleRing.algebraMap_completion_defFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.InfiniteAdeleRing.algebraMap_completionFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.InfiniteAdeleRing.tensorPi_equiv_piTensor_map_mulFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorAuxFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean has no constant by this nameNumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean has no constant by this nameNumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorMulEquivFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean has no constant by this nameNumberField.AdeleRing.DivisionAlgebra.Aux.UfFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.Uf.specFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.UiFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.Ui.specFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.EfamilyFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.E_family_compactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.E_family_nonempty_interiorFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.E_family_unboundedFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.existsEFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.EFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.E_compactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_leftFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.XFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.YFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.X_compactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.Y_compactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernelFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.TFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.T_finite_extracted1FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.T_finiteFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.CFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.C_compactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.incl₂FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.MFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.toQuotFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_contFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.incl₂_isClosedEmbeddingFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.ImAux_isCompactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.M_compactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.rest₁FLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_continuousFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_auxFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_surjectiveFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_equivariantFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.inclD𝔸quotFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuousFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjectiveFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean reported 10 error(s) in this fileNumberField.AdeleRing.DivisionAlgebra._root_.NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompactFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean has no constant by this nameNumberField.AdeleRing.DivisionAlgebra._root_.NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCosetFLT/DivisionAlgebra/Finiteness.lean trust unknown: Lean has no constant by this nameFreyCurve.j_pos_auxFLT/FreyCurve/Basic.lean trust unknown: Lean has no constant by this nameAutomorphicForm.GLn._root_.RingHom.GLFLT/GlobalLanglandsConjectures/GLnDefs.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.ContinuousMulEquiv.isHaarMeasure_comapFLT/HaarMeasure/HaarChar/AddEquiv.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.ContinuousMulEquiv.prodCongrFLT/HaarMeasure/HaarChar/AddEquiv.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.ContinuousMulEquiv.piCongrRightFLT/HaarMeasure/HaarChar/AddEquiv.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.WeaklyLocallyCompactSpace.of_isTopologicalGroup_of_isOpen_compactSpace_subgroupFLT/HaarMeasure/HaarChar/AddEquiv.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.ContinuousLinearEquiv.mulLeftFLT/HaarMeasure/HaarChar/FiniteDimensional.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.ContinuousLinearEquiv.mulRightFLT/HaarMeasure/HaarChar/FiniteDimensional.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRightFLT/HaarMeasure/HaarChar/FiniteDimensional.lean trust unknown: Lean has no constant by this nameMeasureTheory.ringHaarChar_padic_padicIntFLT/HaarMeasure/HaarChar/Padic.lean trust unknown: Lean has no constant by this nameMeasureTheory._root_.QuotientGroup.isUnimodularGroupFLT/HaarMeasure/Quotient.lean trust unknown: Lean has no constant by this nameAlgebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq_auxFLT/HenselianLocalRing/EtaleDecomposition.lean trust unknown: Lean has no constant by this nameAlgebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq'FLT/HenselianLocalRing/EtaleDecomposition.lean trust unknown: Lean has no constant by this nameIdeal.isMaximal_of_isMaximal_under_of_formallyUnramifiedFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileHenselianLocalRing.exists_lift_of_to_ResidueFieldFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileHenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRingFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileIdeal.quotientKerAlgEquivOfSurjective_symm_apply'FLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileModule.finrank_pos_of_freeFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileModule.finrank_eq_one_iff_algebraMap_bijectiveFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileHenselianLocalRing.of_finite_auxFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileIsLocalRing.eq_of_eval_derivative_notMemFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileHenselianLocalRing.eq_of_toAlgHom_residueField_comp_eq_of_isStandardEtaleFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileHenselianLocalRing.eq_of_toAlgHom_residueField_comp_eqFLT/HenselianLocalRing/Finite.lean trust unknown: Lean reported 1 error(s) in this fileTateCurve.Blueprint.hasSum_lattice_prodFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_choose_two_mul_geometricFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_sq_mul_geometric_of_norm_lt_oneFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.sum_int_inv_pow_succFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_int_inv_powFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_comp_negFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_int_inv_pow_subFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_int_inv_pow_subFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_int_inv_pow_negFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_int_inv_pow_neg_oddFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_int_inv_powFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.one_sub_inv_ne_zeroFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.inv_div_one_sub_inv_sqFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.norm_pow_div_one_sub_pow_leFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_aux'FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_auxFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.sum_int_inv_sq'FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_int_inv_sqFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_pnat_of_zeroFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_pnat_coe_mul_geometricFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_corr_natFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_V_natFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_corr_intFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_corr_intFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.norm_mul_lt_oneFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.norm_mul_inv_lt_oneFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.zpow_neg_natCast_mulFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_VFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.im_sub_int_mul_ne_zeroFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.corrector_row_evalFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.inv_sq_div_one_sub_inv_cubeFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.inv_mul_one_add_inv_div_one_sub_inv_cubeFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.div_sq_add_two_mul_div_cubeFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.sum_int_inv_cube'FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_V₂FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.sum_int_inv_fourthFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_int_inv_fourthFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.not_summable_natCast_powFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_natCast_pow_mul_oneFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_tsum_pow_eq_sAnFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_int_lambert_natAbsFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.row_eval_ne_zeroFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.G_q_expansionFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.bernoulli'_fiveFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.bernoulli'_sixFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.sum_int_inv_sixthFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_int_inv_sixthFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.log_div_two_pi_I_imFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.e_log_div_two_pi_IFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.notMem_lattice_of_im_betweenFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.analytic_weierstrass_algebraFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.analytic_weierstrass_of_expFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAtHomFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAtHom_applyFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAtHom_ratFuncXFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_pnat_of_natFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_nat_of_pnat_addFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.tsum_int_decompFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_pnat_lambert₁FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_pnat_lambert₂FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_pnat_lambert₂'FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.norm_pow_mul_lt_oneFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.cast_le_sqFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.choose_two_le_sqFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.choose_add_one_two_le_sqFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_coeff_prodFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_prod_pnatFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_prod_lambertFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_divisor_collectFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_prodCFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.coeff_X_of_neFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_coeff_X_zeroFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_coeff_XFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.coeff_Y_of_neFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_coeff_Y_zeroFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_coeff_YFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_ratCastFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.summable_sAn_termsFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.ofNat_powerSeries_eq_CFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.coeff_a₆FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_coeff_a₆FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.coeff_a₄FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.evalAt_coeff_a₄FLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.coeffs_eq_zero_of_hasSum_puncturedFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.ratFunc_eq_zero_of_evalAt_eq_zero_on_infiniteFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_evalAt_addFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_evalAt_negFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_evalAt_subFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.hasSum_evalAt_mulFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this nameTateCurve.Blueprint.transcendental_punctured_unit_disk_infiniteFLT/KnownIn1980s/EllipticCurves/TateCurveConstruction.lean trust unknown: Lean has no constant by this name_root_.LinearEquiv.mulLeftFLT/Mathlib/Algebra/Algebra/Bilinear.lean trust unknown: Lean has no constant by this name_root_.LinearEquiv.mulRightFLT/Mathlib/Algebra/Algebra/Bilinear.lean trust unknown: Lean has no constant by this name_root_.QuotientGroup.quotientConjActEquivImageMulSingletonFLT/Mathlib/GroupTheory/DoubleCoset.lean trust unknown: Lean has no constant by this name_root_.MeasurableEmbedding.isMulLeftInvariant_comapFLT/Mathlib/MeasureTheory/Group/Action.lean trust unknown: Lean has no constant by this name_root_.MeasurableEmbedding.isMulRightInvariant_comapFLT/Mathlib/MeasureTheory/Group/Action.lean trust unknown: Lean has no constant by this namePadicInt._root_.AddSubgroup.comap_smul_oneFLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean trust unknown: Lean has no constant by this nameContinuousCohomology._root_.TopRep.homogeneousCochains.d_comp_d_applyFLT/Mathlib/RepresentationTheory/Homological/ContCohomology/Basic.lean trust unknown: Lean has no constant by this nameContinuousSemialgHom._root_.ContinuousSemialgHomClass.toContinuousSemialgHomFLT/Mathlib/Topology/Algebra/Algebra/Hom.lean trust unknown: Lean has no constant by this nameIsModuleTopology._root_.Algebra.moduleTopology_leFLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean trust unknown: Lean has no constant by this nameIsModuleTopology._root_.moduleTopology.transFLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean trust unknown: Lean has no constant by this nameIsModuleTopology._root_.Prod.instFinite_leftAlgebraFLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean trust unknown: Lean has no constant by this nameIsModuleTopology._root_.Prod.instFinite_rightAlgebraFLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean trust unknown: Lean has no constant by this nameIsModuleTopology._root_.Module.Finite.secondCountabletopologyFLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean trust unknown: Lean has no constant by this nameRestrictedProduct._root_.LinearEquiv.restrictedProductPiFLT/Mathlib/Topology/Algebra/RestrictedProduct/Module.lean trust unknown: Lean has no constant by this nameRestrictedProduct._root_.ContinuousLinearEquiv.restrictedProductPiFLT/Mathlib/Topology/Algebra/RestrictedProduct/Module.lean trust unknown: Lean has no constant by this nameconstant_approxFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namelog_approxFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_strictMono_aux3FLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_strictMono_aux2FLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_strictMono_auxFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_four_ltFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_five_gtFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_thirteen_ltFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this namerootDiscrBound_fourteen_gtFLT/NumberField/DiscriminantBounds.lean trust unknown: Lean has no constant by this nameIsDedekindDomain.FiniteAdeleRing._root_.RestrictedProduct.mulSingleHomFLT/QuaternionAlgebra/NumberField.lean trust unknown: Lean has no constant by this nameDimensionTheorem.hilbertSamuel_zeroFLT/Slop/DimensionTheorem/DimLeGrowth.lean trust unknown: Lean has no constant by this nameDimensionTheorem.hilbertSamuel_coeFLT/Slop/DimensionTheorem/DimLeGrowth.lean trust unknown: Lean has no constant by this nameDimensionTheorem.map_mk_maximalIdealFLT/Slop/DimensionTheorem/DimLeGrowth.lean trust unknown: Lean has no constant by this nameDimensionTheorem.length_quotient_map_quotientFLT/Slop/DimensionTheorem/DimLeGrowth.lean trust unknown: Lean has no constant by this nameDimensionTheorem.hilbertSamuel_quotient_eqFLT/Slop/DimensionTheorem/DimLeGrowth.lean trust unknown: Lean has no constant by this nameDimensionTheorem.multiset_prod_mem_powFLT/Slop/DimensionTheorem/GrowthLeDelta.lean trust unknown: Lean has no constant by this nameDimensionTheorem.monomialFLT/Slop/DimensionTheorem/GrowthLeDelta.lean trust unknown: Lean has no constant by this nameDimensionTheorem.monomial_memFLT/Slop/DimensionTheorem/GrowthLeDelta.lean trust unknown: Lean has no constant by this nameDimensionTheorem.span_pow_eq_span_monomialFLT/Slop/DimensionTheorem/GrowthLeDelta.lean trust unknown: Lean has no constant by this nameDimensionTheorem.length_span_range_leFLT/Slop/DimensionTheorem/GrowthLeDelta.lean trust unknown: Lean has no constant by this nameDimensionTheorem.GrowthLE.telescope_auxFLT/Slop/DimensionTheorem/Numeric.lean trust unknown: Lean has no constant by this nameDimensionTheorem.multichoose_le_powFLT/Slop/DimensionTheorem/Numeric.lean trust unknown: Lean has no constant by this nameDickson.factorization_60_2FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this nameDickson.factorization_60_3FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this nameDickson.factorization_60_5FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this nameDickson.factorization_30_3FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this nameDickson.factorization_30_5FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this nameDickson.factorization_15_5FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this nameDickson.factorization_15_3FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean trust unknown: Lean has no constant by this name
Depend on extra axioms (49)
knownin1980sFLT/Assumptions/KnownIn1980s.lean extra axioms: knownin1980sMazur_statementFLT/Assumptions/Mazur.lean extra axioms: Mazur_statementOdlyzko_statementFLT/Assumptions/Odlyzko.lean extra axioms: Odlyzko_statementTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isFiniteRelIndex_ΔFLT/AutomorphicForm/QuaternionAlgebra/Basic.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.apply_eq_smulFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalarFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T_smul_defFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.U_smul_defFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.formMap_smulFLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.sum_filter_map_eq_ΔIndex_div_ΔIndexFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_map_le_mapFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_leFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eqFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_def_of_memFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_coeFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_defFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.inner_smul_eq_inner_inv_smulFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.inner_adicCompletion_smulFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.inner_heckeOperatorFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.adjoint_heckeOperatorLFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.isSymmetric_toModuleEnd_TFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.EigenformFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenspaceFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.mem_eigenspace_iffFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenvalueFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.mem_eigenspace_iff_TFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenvalue_injectiveFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenSpace_ne_botFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.existsFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.isInternalFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.cardinalMk_leFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integersFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegersFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeQuotientFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeQuotient_mkFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegers_surjectiveFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenformFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform_applyFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalar_tmulFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform_injectiveFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.pi_lift_injectiveFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.tensorEquivPiFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.tensorEquivPi_tmul_applyFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.equivAlgHomFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.under_primeFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.prime_mem_minimalPrimesFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists_le_of_isPrimeFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980sTotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists_of_isPrimeFLT/AutomorphicForm/QuaternionAlgebra/InnerProduct.lean extra axioms: knownin1980s
Depend on sorry (90)
HurwitzRatHat.injective_hRatFLT/Data/HurwitzRatHat.leanHurwitzRatHat.injective_zHatFLT/Data/HurwitzRatHat.leanHurwitzRatHat.canonicalFormFLT/Data/HurwitzRatHat.leanHurwitzRatHat.completed_unitsFLT/Data/HurwitzRatHat.leanQHat.unitsrat_join_unitszHatFLT/Data/QHat.leanIsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToPiRightFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletionFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletion_range_eq_integersFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_mul_inertiaDeg_eq_finrankFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletionFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_bijectiveFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquivFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquivFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquivFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv_tmul_applyFLT/DedekindDomain/Completion/BaseChange.leanIsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv_bijOnFLT/DedekindDomain/Completion/BaseChange.leanDeformation.flatFunctorFLT/Deformations/LiftFunctor.leanDeformation.isCorepresentable_deformationFunctorFLT/Deformations/Representable.leanDeformation.SLiftFunctorFLT/Deformations/Representable.leanDeformation.narrowSLiftFunctorFLT/Deformations/Representable.leanDeformation.isCorepresentable_narrowSLiftFunctorFLT/Deformations/Representable.leanDeformation.narrowSLiftUniversalRingFLT/Deformations/Representable.leanDeformation.narrowSLiftUniversalRingCorepresentableByFLT/Deformations/Representable.leanNumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mulFLT/DivisionAlgebra/Finiteness.leanNumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mulFLT/DivisionAlgebra/Finiteness.leanNumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_rightFLT/DivisionAlgebra/Finiteness.leanNumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'FLT/DivisionAlgebra/Finiteness.leanNumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_CFLT/DivisionAlgebra/Finiteness.leanNumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_surjectiveFLT/DivisionAlgebra/Finiteness.leanNumberField.AdeleRing.DivisionAlgebra.compact_quotientFLT/DivisionAlgebra/Finiteness.leanWeierstrassCurve.n_torsion_finiteFLT/EllipticCurve/Torsion.leanWeierstrassCurve.n_torsion_cardFLT/EllipticCurve/Torsion.leangroup_theory_lemmaFLT/EllipticCurve/Torsion.leanWeierstrassCurve.n_torsion_dimensionFLT/EllipticCurve/Torsion.leanWeierstrassCurve.galoisRepresentationFLT/EllipticCurve/Torsion.leanWeierstrassCurve.galoisRepFLT/EllipticCurve/Torsion.leanFreyPackage.mazurFLT/FreyCurve/Mazur.leancyclic_base_changeFLT/GaloisRepresentation/Automorphic.leanGaloisRepresentation.IsHardlyRamified.mem_isCompatibleFLT/GaloisRepresentation/HardlyRamified/Family.leanFreyCurve.torsion_isHardlyRamifiedFLT/GaloisRepresentation/HardlyRamified/Frey.leanFreyCurve.torsion_not_isIrreducibleFLT/GaloisRepresentation/HardlyRamified/Frey.leanGaloisRepresentation.IsHardlyRamified.liftsFLT/GaloisRepresentation/HardlyRamified/Lift.leanGaloisRepresentation.IsHardlyRamified.mod_threeFLT/GaloisRepresentation/HardlyRamified/ModThree.leanGaloisRepresentation.IsHardlyRamified.three_adicFLT/GaloisRepresentation/HardlyRamified/Threeadic.leanIsDedekindDomain.diamond_fixFLT/GlobalLanglandsConjectures/GLnDefs.leanAutomorphicForm.GLn.actionTensorCAlgFLT/GlobalLanglandsConjectures/GLnDefs.leanAutomorphicForm.GLn.actionTensorCAlg'FLT/GlobalLanglandsConjectures/GLnDefs.leanAutomorphicForm.GLn.actionTensorCAlg'2FLT/GlobalLanglandsConjectures/GLnDefs.leanAutomorphicForm.GLn.actionTensorCAlg'3FLT/GlobalLanglandsConjectures/GLnDefs.leanAutomorphicForm.GLn.Weight.IsTrivialFLT/GlobalLanglandsConjectures/GLzero.leanAutomorphicForm.GL0.ofComplexFLT/GlobalLanglandsConjectures/GLzero.leanAutomorphicForm.GL0.classificationFLT/GlobalLanglandsConjectures/GLzero.leanAutomorphicForm.GLn.ofComplexFLT/GlobalLanglandsConjectures/GLzero.leanAutomorphicForm.GLn.classificationFLT/GlobalLanglandsConjectures/GLzero.leanHenselianLocalRing.of_finiteFLT/HenselianLocalRing/Finite.leanHenselianLocalRing.exist_residueFieldMap_eq_of_etaleFLT/HenselianLocalRing/Finite.leanHenselianLocalRing.eq_of_residueFieldMap_eqFLT/HenselianLocalRing/Finite.leanHenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etaleFLT/HenselianLocalRing/Finite.leanWeierstrassCurve.torsion_flat_of_good_reductionFLT/KnownIn1980s/EllipticCurves/Flat.leanWeierstrassCurve.resultant_Φ_ΨSqFLT/KnownIn1980s/EllipticCurves/Flat.leanWeierstrassCurve.isCoprime_Φ_ΨSqFLT/KnownIn1980s/EllipticCurves/Flat.leanWeierstrassCurve.torsion_unramified_of_good_reductionFLT/KnownIn1980s/EllipticCurves/GoodReduction.leanWeierstrassCurve.tateCurveEquivFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tateEquivFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.exists_variableChange_tateCurveFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tateEquiv_baseChangeFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tateEquiv_galoisFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tateEquivSepClosureFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tatePointFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tatePoint_baseChangeFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tatePoint_galoisFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tatePoint_mem_torsionBy_of_mem_rootsOfUnityFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.tatePoint_mem_torsionBy_of_pow_eqFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.weilPairing_tatePointFLT/KnownIn1980s/EllipticCurves/TateCurve.leanWeierstrassCurve.torsion_rank_twoFLT/KnownIn1980s/EllipticCurves/Torsion.leanWeierstrassCurve.weilPairingFLT/KnownIn1980s/EllipticCurves/WeilPairing.leanDickson.classification_tameFLT/KnownIn1980s/PGL2/Defs.leanDickson.classification_wildFLT/KnownIn1980s/PGL2/Defs.leanGroup.subsingleton_of_pow_prime_eq_oneFLT/Patching/Utils/CompactHausdorffRings.leanGroup.totallyDisconnected_of_pow_prime_eq_oneFLT/Patching/Utils/CompactHausdorffRings.leanGroup.rootableFLT/Patching/Utils/CompactHausdorffRings.leanCommGroup.no_compact_automorphismsFLT/Patching/Utils/CompactHausdorffRings.leanFLT.Bosses.B4FLT/Proof.leanFLT.Bosses.B4_implies_B3FLT/Proof.leanFLT.Bosses.B4_proofFLT/Proof.leanFLT.Bosses.B3_proofFLT/Proof.leanFLT.Bosses.B2_proofFLT/Proof.leanFLT.Bosses.B1_proofFLT/Proof.leanfltFLT/Proof.leanPNat.pow_add_pow_ne_powFermatsLastTheorem.lean