From 51044046880f105a0486a4b2a25774a2cdf2e4c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 30 Oct 2023 15:19:21 +0000 Subject: [PATCH] Blueprint: Fix links to Lean declarations --- .../NumberTheory/LegendreSymbol/AddChar/Basic.lean | 8 ++++---- blueprint/src/ap.tex | 2 +- blueprint/src/chang.tex | 4 ++-- blueprint/src/ff.tex | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean b/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean index 6e00ce2050..5e1f0ffe72 100644 --- a/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean +++ b/LeanAPAP/Mathlib/NumberTheory/LegendreSymbol/AddChar/Basic.lean @@ -13,10 +13,10 @@ Rename * `map_add_mul` → `map_add_eq_mul` * `map_zero_one` → `map_zero_eq_one` * `map_nsmul_pow` → `map_nsmul_eq_pow` -* `coe_to_fun_apply` → whatever is better, maybe change to `ψ.to_monoid_hom a = ψ (of_mul a)`. +* `coe_toFun_apply` → whatever is better, maybe change to `ψ.toMonoidNom a = ψ (of_mul a)`. -Kill the evil instance `add_char.monoid_hom_class`. It creates a diamond for -`fun_like (add_char G R) _ _`. +Kill the evil instance `AddChar.MonoidHomClass`. It creates a diamond for +`FunLike (AddChar G R) _ _`. -/ --TODO: This instance is evil @@ -39,7 +39,7 @@ instance instFunLike : FunLike (AddChar G R) G fun _ ↦ R where coe := (⇑) coe_injective' ψ χ h := by obtain ⟨⟨_, _⟩, _⟩ := ψ; congr --- TODO: Replace `add_char.to_monoid_hom` +-- TODO: Replace `AddChar.toMonoidHom` /-- Interpret an additive character as a monoid homomorphism. -/ def toMonoidHom' : AddChar G R ≃ (Multiplicative G →* R) := Equiv.refl _ diff --git a/blueprint/src/ap.tex b/blueprint/src/ap.tex index 17d4af8e76..7306d3f994 100644 --- a/blueprint/src/ap.tex +++ b/blueprint/src/ap.tex @@ -110,7 +110,7 @@ \chapter{Almost-Periodicity} \begin{theorem}[$L_p$ almost periodicity] \label{lp_ap} -\lean{almost_periodicity} +\lean{AlmostPeriodicity.almost_periodicity} \leanok Let $\epsilon\in (0,1]$ and $m\geq 1$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$. Let $f:G\to \bbc$. There exists $T\subseteq G$ such that diff --git a/blueprint/src/chang.tex b/blueprint/src/chang.tex index 0d1b5f6eb8..a7ccb30685 100644 --- a/blueprint/src/chang.tex +++ b/blueprint/src/chang.tex @@ -85,7 +85,7 @@ \chapter{Chang's lemma} \begin{definition}[Energy] \label{energy} \uses{weight_energy} -\lean{boring_energy} +\lean{boringEnergy} \leanok Let $G$ be a finite abelian group and $A\subseteq G$. Let $m\geq 1$. We define \[E_{2m}(A)=\sum_{a_1,\ldots,a_{2m}\in A}1_{a_1+\cdots-a_{2m}=0}.\] @@ -146,7 +146,7 @@ \chapter{Chang's lemma} \begin{lemma} \label{energy_alt} \uses{energy} -\lean{boring_energy_eq} +\lean{boringEnergy_eq} \leanok If $A\subset G$ and $m\geq 1$ then \[E_{2m}(A) = \sum_x 1_A^{(m)}(x)^2.\] diff --git a/blueprint/src/ff.tex b/blueprint/src/ff.tex index 18a33fce85..3811a16478 100644 --- a/blueprint/src/ff.tex +++ b/blueprint/src/ff.tex @@ -172,7 +172,7 @@ \chapter{Finite field model} \begin{lemma} \label{no3aps_inner_prod} -\lean{add_salem_spencer.L2inner_mu_conv_mu_mu_two_smul_mu} +\lean{AddSalemSpencer.l2inner_mu_conv_mu_mu_two_smul_mu} \leanok If $A\subseteq G$ has no non-trivial three-term arithmetic progressions and $G$ has odd order then \[\langle \mu_A\ast \mu_A,\mu_{2\cdot A}\rangle = 1/\abs{A}^2.\]