FLT/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Height One Spectrum

Material destined for Mathlib.

Imports (4)
Imported by 2 files
  1. instance Rat.HeightOneSpectrum.IsIntegralClosure.(instance at line 29) line 29 source
  2. instance Rat.HeightOneSpectrum.IsIntegralClosure.(instance at line 31) line 31 source
  3. instance Rat.HeightOneSpectrum.IsIntegralClosure.(instance at line 33) line 33 source
  4. theorem Rat.HeightOneSpectrum.IsIntegralClosure.intEquiv_apply_coe line 36 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, Eq, RingEquiv, Rat.IsIntegralClosure.intEquiv

    Proof uses: RingEquiv.symm, Exists, RingEquiv.surjective, of_eq_true, Eq.trans, True, congr, congrArg, eq_intCast, map_intCast, eq_self

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  5. theorem Rat.HeightOneSpectrum.pow_natGenerator_dvd_iff line 46 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, IsDedekindDomain.HeightOneSpectrum, Nat, Iff, Dvd.dvd, HPow.hPow, Rat.HeightOneSpectrum.natGenerator, Membership.mem, Ideal, Ideal.map, RingEquiv, Rat.IsIntegralClosure.intEquiv, IsDedekindDomain.HeightOneSpectrum.asIdeal

    Proof uses: Eq.mpr, Ideal.span, Singleton.singleton, Set, id, Eq, congrArg, Eq.symm, Rat.HeightOneSpectrum.span_natGenerator, Ideal.span_singleton_pow, propext, Ideal.mem_span_singleton, Iff.symm, Int.ofNat_dvd

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  6. theorem Rat.HeightOneSpectrum.natGenerator_eq_absNorm line 53 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, IsDedekindDomain, IsDedekindDomain.HeightOneSpectrum, Eq, Nat, Rat.HeightOneSpectrum.natGenerator, MonoidWithZeroHom, Ideal, Ideal.absNorm, Rat.HeightOneSpectrum.instInfinite, IsDedekindDomain.HeightOneSpectrum.asIdeal

    Proof uses: Eq.mpr, Int.natAbs, Submodule.IsPrincipal.generator, Ideal.map, RingEquiv, Rat.IsIntegralClosure.intEquiv, id, congrArg, Rat.HeightOneSpectrum.natGenerator.eq_1, Ideal.span, Singleton.singleton, Set, Submodule, Submodule.IsPrincipal, Eq.trans, Eq.symm, Int.ideal_span_absNorm_eq_self, Eq.refl, Eq.rec, Iff.mpr and 25 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

  7. theorem Rat.HeightOneSpectrum.intValuation_eq_padicValuation_iff_multiplicity_eq_multiplicity line 72 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, IsDedekindDomain, IsDedekindDomain.HeightOneSpectrum, Ne, OfNat.ofNat, Iff, Eq, WithZero, Multiplicative, Valuation, IsDedekindDomain.HeightOneSpectrum.intValuation, Rat.padicValuation, Nat, Nat.Prime, Equiv, Nat.Primes and 10 more

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Neg.neg, WithZero.exp, congr, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_coe_neg_multiplicity, ite, padicValRat, ite_eq_right_of_eq_false, False, eq_false, padicValInt, padicValRat.of_int, Nat.padicValNat_def, iff_self

    132 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  8. theorem Rat.HeightOneSpectrum.valuation_apply_coe_eq_padicValuation line 83 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, IsDedekindDomain, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Eq, WithZero, Multiplicative, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, RingHom, Algebra.algebraMap, Rat.padicValuation, Nat, Nat.Prime, Equiv, Nat.Primes and 3 more

    Proof uses: Eq.mpr, IsDedekindDomain.HeightOneSpectrum.intValuation, id, congrArg, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, OfNat.ofNat, Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congr, map_zero, Int.cast_zero, eq_self, Eq.symm, multiplicity, Ideal, IsDedekindDomain.HeightOneSpectrum.asIdeal and 38 more

    153 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

    Open to load the checked before-and-after goal states.

  9. theorem Rat.HeightOneSpectrum.valuation_apply_eq_padicValuation line 94 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, IsDedekindDomain, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Eq, WithZero, Multiplicative, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, Rat.padicValuation, Nat, Nat.Prime, Equiv, Nat.Primes, Rat.HeightOneSpectrum.primesEquiv

    Proof uses: Prod, Subtype, Membership.mem, Submonoid, nonZeroDivisors, HMul.hMul, RingHom, Algebra.algebraMap, Prod.snd, Prod.fst, Exists, IsLocalization.surj, Prod.mk, Subtype.mk, IsLocalization.mk', of_eq_true, Eq.trans, HDiv.hDiv, True, congr and 16 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  10. theorem Rat.HeightOneSpectrum.adicCompletion.padicEquiv_cast line 101 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Algebra, Rat, IsIntegralClosure, Int, IsDedekindDomain, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, WithVal, WithZero, Multiplicative, IsDedekindDomain.HeightOneSpectrum.valuation, Eq, Padic, Nat, Nat.Prime, Equiv, Nat.Primes, Rat.HeightOneSpectrum.primesEquiv, instFactPrimeValNat and 12 more

    Proof uses: Eq.refl

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  11. lemma Rat.HeightOneSpectrum.adicCompletion.padicEquiv_norm_coe_eq line 109 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Rat, WithVal, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, Eq, Real, Norm.norm, Padic, Nat, Nat.Prime, Equiv, Nat.Primes, Rat.HeightOneSpectrum.primesEquiv, instFactPrimeValNat, ContinuousAlgEquiv, IsDedekindDomain.HeightOneSpectrum.adicCompletion and 5 more

    Proof uses: Eq.mpr, RingEquiv, Valuation.Completion, Rat.padicValuation, Padic.withValRingEquiv, UniformEquiv, UniformSpace.Completion, UniformSpace.Completion.mapEquiv, Rat.HeightOneSpectrum.withValEquiv, id, congrArg, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_cast, UniformSpace.Completion.mapEquiv_coe, UniformSpace.Completion.extension, Function.comp, WithVal.equiv, Padic.coe_withValRingEquiv, UniformSpace.Completion.extension_coe, IsUniformInducing.uniformContinuous, RingHom.comp and 88 more

    248 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

  12. lemma Rat.HeightOneSpectrum.adicCompletion.padicEquiv_norm_eq line 128 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Rat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, Real, Norm.norm, Padic, Nat, Nat.Prime, Equiv, Nat.Primes, Rat.HeightOneSpectrum.primesEquiv, instFactPrimeValNat, ContinuousAlgEquiv, Rat.HeightOneSpectrum.adicCompletion.padicEquiv, Rat.HeightOneSpectrum.instInfinite

    Proof uses: Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion, Exists, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective, UniformSpace.Completion.induction_on, WithVal, isClosed_eq, UniformSpace.Completion, Continuous.comp, continuous_norm, ContinuousAlgEquiv.continuous, IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion, Eq.mpr, RingHom, Algebra.algebraMap, id and 5 more

    97 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.