Zulip Chat Archive

Stream: mathlib4

Topic: Some elementary number theory results

Michael Stoll (Mar 15 2025 at 22:59):

When formalizing proofs for an olympiad-style problem ("if a natural number $n$ divides $2^n-1$ , it follows that $n \le 1$ "), I found the following results helpful, which look like they might be useful additions to Mathlib.

But before trying to PR them, I'd like to ask for opinions here.

import Mathlib

open Nat

lemma natCard_units_lt (M : Type*) [MonoidWithZero M] [Nontrivial M] [Finite M] :
    Nat.card Mˣ < Nat.card M := by
  have : Fintype M := Fintype.ofFinite M
  simpa only [Fintype.card_eq_nat_card] using card_units_lt M
-- #find_home natCard_units_lt -- [Mathlib.RingTheory.Fintype]

lemma orderOf_lt_card {M : Type*} [MonoidWithZero M] [Nontrivial M] [Finite M] (a : M) :
    orderOf a < Nat.card M := by
  have : Fintype M := Fintype.ofFinite M
  by_cases h : IsUnit a
  · rw [← h.unit_spec, orderOf_units]
    exact orderOf_le_card.trans_lt <| natCard_units_lt M
  · rw [orderOf_eq_zero_iff'.mpr fun n hn ha ↦ h <| IsUnit.of_pow_eq_one ha hn.ne']
    exact card_pos
-- #find_home orderOf_lt_card -- [Mathlib.RingTheory.Fintype]

lemma ZMod.orderOf_lt {n : ℕ} (hn : 1 < n) (a : ZMod n) : orderOf a < n :=
  have : NeZero n := ⟨by omega⟩
  have : Nontrivial (ZMod n) := nontrivial_iff.mpr hn.ne'
  calc
  orderOf a < Nat.card (ZMod n) := orderOf_lt_card a
  _         = n                 := card_zmod n

lemma ZMod.one_eq_zero_iff {n : ℕ} : (1 : ZMod n) = 0 ↔ n = 1 := by
  rw [← Nat.cast_one, natCast_zmod_eq_zero_iff_dvd, dvd_one]
-- #find_home ZMod.one_eq_zero_iff -- [Mathlib.Data.ZMod.Basic]

lemma Nat.gcd_eq_one_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : n.gcd m = 1 := by
  rw [← coprime_iff_gcd_eq_one, ← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]
  push_neg
  exact fun p hp hn hm ↦
    ((le_of_dvd (by omega) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false
-- #find_home Nat.gcd_eq_one_of_lt_minFac -- [Mathlib.Data.Nat.Prime.Basic]

Kevin Buzzard (Mar 15 2025 at 23:40):

They all look great to me!

Michael Stoll (Mar 16 2025 at 23:19):

#22989
(Off-topic question: Why is there a CI step Add the "awaiting-CI" label (that spits out a screenfull of HTML), when actually that label is getting removed?)

Bryan Gin-ge Chen (Mar 16 2025 at 23:21):

@Michael Rothgang added that to make things easier for the dashboard, I think.

Michael Stoll (Mar 16 2025 at 23:25):

So when would it add the label? It is almost the last step within build, so at this point, CI will have succeeded unless there was an error before. (And the HTML contains the line

<title>Forbidden &middot; GitHub</title>

which seems rather strange...)

Bryan Gin-ge Chen (Mar 16 2025 at 23:27):

I'll let Michael answer those questions when he's around, but the PR was here: #21881

Michael Stoll (Mar 17 2025 at 00:37):

The full output of this step on the PR is

Run curl --request ADD \
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0

<!DOCTYPE html>
<html>
  <head>
    <meta content="origin" name="referrer">
    <title>Forbidden &middot; GitHub</title>
    <style type="text/css" media="screen">
      body {
        background-color: #f1f1f1;
        margin: 0;
      }
      body,
      input,
      button {
        font-family: "Helvetica Neue", Helvetica, Arial, sans-serif;
      }
      .container { margin: 30px auto 40px auto; width: 800px; text-align: center; }
      a { color: #4183c4; text-decoration: none; font-weight: bold; }
      a:hover { text-decoration: underline; }
      h1, h2, h3 { color: #666; }
      ul { list-style: none; padding: 25px 0; }
      li {
        display: inline;
        margin: 10px 50px 10px 0px;
      }
      .logo { display: inline-block; margin-top: 35px; }
      .logo-img-2x { display: none; }
      @media
      only screen and (-webkit-min-device-pixel-ratio: 2),
      only screen and (   min--moz-device-pixel-ratio: 2),
      only screen and (     -o-min-device-pixel-ratio: 2/1),
      only screen and (        min-device-pixel-ratio: 2),
      only screen and (                min-resolution: 192dpi),
      only screen and (                min-resolution: 2dppx) {
        .logo-img-1x { display: none; }
        .logo-img-2x { display: inline-block; }
      }
    </style>
  </head>
  <body>

    <div class="container">
      <h1>Access to this site has been restricted.</h1>

      <p>
        <br>
        If you believe this is an error,
        please contact <a href="https://support.github.com">Support</a>.
      </p>

      <div id="s">
        <a href="https://githubstatus.com">GitHub Status</a> &mdash;
        <a href="https://twitter.com/githubstatus">@githubstatus</a>
      </div>
    </div>
  </body>
</html>
100  1812    0  1812    0     0  40347      0 --:--:-- --:--:-- --:--:-- 41181

To me, this looks like an error message from github...

Michael Rothgang (Mar 17 2025 at 14:36):

Short version: yes, the PR was meant to make the queueboard more reliable. As you noticed, it doesn't do what it should, though. I've filed #23010 to revert it.

Last updated: May 02 2025 at 03:31 UTC