CyclotomicRemainder.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Scalar divisibility and monic remainders

The canonical remainder map for a monic root extension is linear over the coefficient ring. Consequently, divisibility by a scalar in the extension is equivalent to divisibility of every coefficient of the monic remainder.

The actual polynomial quotient AdjoinRoot f is such an extension; no additional representation hypothesis is required.

theorem OAI.CirculantHadamard.CyclotomicRemainder.C_dvd_modByMonic_of_dvd_map line 28
Source documentation
Scalar divisibility in a monic root extension gives a constant-polynomial factor of the canonical remainder.
```
theorem C_dvd_modByMonic_of_dvd_map (h : IsAdjoinRootMonic S f)
    (a : R) (F : R[X]) (hdiv : algebraMap R S a ∣ h.map F) :
    C a ∣ F %ₘ f := by
…
```
theorem OAI.CirculantHadamard.CyclotomicRemainder.dvd_map_of_C_dvd_modByMonic line 41
Source documentation
A constant factor of the canonical remainder gives scalar divisibility after passing to the monic root extension.
```
theorem dvd_map_of_C_dvd_modByMonic (h : IsAdjoinRootMonic S f)
    (a : R) (F : R[X]) (hdiv : C a ∣ F %ₘ f) :
    algebraMap R S a ∣ h.map F := by
…
```
theorem OAI.CirculantHadamard.CyclotomicRemainder.map_dvd_iff_C_dvd_modByMonic line 52
Source documentation
Exact divisibility equivalence for a monic root extension.
```
theorem map_dvd_iff_C_dvd_modByMonic (h : IsAdjoinRootMonic S f)
    (a : R) (F : R[X]) :
    algebraMap R S a ∣ h.map F ↔ C a ∣ F %ₘ f :=
…
```
theorem OAI.CirculantHadamard.CyclotomicRemainder.map_dvd_iff_dvd_coeff_modByMonic line 59
Source documentation
Scalar divisibility is equivalent to divisibility of every coefficient of the canonical remainder.
```
theorem map_dvd_iff_dvd_coeff_modByMonic (h : IsAdjoinRootMonic S f)
    (a : R) (F : R[X]) :
    algebraMap R S a ∣ h.map F ↔ ∀ i, a ∣ (F %ₘ f).coeff i :=
…
```

theorem OAI.CirculantHadamard.CyclotomicRemainder.dvd_coeff_modByMonic_of_dvd_map line 65

Source documentation

Coefficient form of the forward divisibility bridge.

theorem dvd_coeff_modByMonic_of_dvd_map (h : IsAdjoinRootMonic S f)
    (a : R) (F : R[X]) (hdiv : algebraMap R S a ∣ h.map F) (i : ℕ) :
    a ∣ (F %ₘ f).coeff i :=
…

theorem OAI.CirculantHadamard.CyclotomicRemainder.adjoinRoot_dvd_iff_C_dvd_modByMonic line 72
Source documentation
The actual quotient by a monic polynomial satisfies the constant-factor criterion, using its concrete IsAdjoinRootMonic constructor.
```
theorem adjoinRoot_dvd_iff_C_dvd_modByMonic (f : R[X]) (hf : f.Monic)
    (a : R) (F : R[X]) :
    algebraMap R (AdjoinRoot f) a ∣ AdjoinRoot.mk f F ↔ C a ∣ F %ₘ f := by
…
```
theorem OAI.CirculantHadamard.CyclotomicRemainder.adjoinRoot_dvd_iff_dvd_coeff_modByMonic line 81
Source documentation
The concrete monic quotient has scalar divisibility exactly when all coefficients of the monic remainder have that scalar factor.
```
theorem adjoinRoot_dvd_iff_dvd_coeff_modByMonic (f : R[X]) (hf : f.Monic)
    (a : R) (F : R[X]) :
    algebraMap R (AdjoinRoot f) a ∣ AdjoinRoot.mk f F ↔
      ∀ i, a ∣ (F %ₘ f).coeff i :=
…
```

theorem OAI.CirculantHadamard.CyclotomicRemainder.adjoinRoot_dvd_coeff_modByMonic line 90

Source documentation

Scalar divisibility in a monic quotient implies coefficientwise divisibility of the remainder.

theorem adjoinRoot_dvd_coeff_modByMonic (f : R[X]) (hf : f.Monic)
    (a : R) (F : R[X])
    (hdiv : algebraMap R (AdjoinRoot f) a ∣ AdjoinRoot.mk f F) (i : ℕ) :
    a ∣ (F %ₘ f).coeff i :=
…