Revision #3183 → #4056 · back to history
modifiedClass group G_Δ of binary quadratic forms86f44a40a00e
| Field | From #3183 | To #4056 |
|---|
| mathlib.module | Mathlib.RingTheory.ClassGroup | Mathlib.RingTheory.ClassGroup.Basic |
modifiedSet P_Δ of primes with Kronecker symbol 1cd425212d7de
| Field | From #3183 | To #4056 |
|---|
| mathlib.decl | — | jacobiSym |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol |
| note | Grep for `kroneckerSymbol`/`KroneckerSymbol` returned no Mathlib matches. | Mathlib has `jacobiSym` (and `legendreSym`); the Kronecker symbol specifically is not a named decl, so this is a generalization. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
addedEmpty product convention for 1e2ce453fff82
addedPrimality decidable in polynomial time (AKS)11a77ac6fa18
addedKronecker symbol (Δ/q)5e0cb28d5ac7
added2-Sylow subgroup of the class group6a28d0430292