CyclicScalarDivision.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Division by regular coefficient scalars in an additive monoid algebra

A finite group algebra usually has zero divisors. A nonzero scalar from a domain nevertheless acts injectively, as is seen separately at each coefficient. This is the cancellation needed when the projected norm equation is divided by one power of the residue characteristic.

theorem OAI.CirculantHadamard.scalar_division_exists line 26
Source documentation
Coefficientwise divisibility produces an actual element of the finite group algebra whose scalar multiple is the original element.
```
theorem scalar_division_exists (p : R) (F : AddMonoidAlgebra R G)
    (hF : ∀ g, p ∣ F.coeff g) :
    ∃ F' : AddMonoidAlgebra R G, F = AddMonoidAlgebra.single (0 : G) p * F' := by
…
```
theorem OAI.CirculantHadamard.scalar_division_coefficients line 40
Source documentation
Multiplication by a scalar makes every coefficient divisible by that scalar.
```
theorem scalar_division_coefficients [Finite G] (p : R) (F : AddMonoidAlgebra R G) :
    ∀ g, p ∣ (AddMonoidAlgebra.single (0 : G) p * F).coeff g := by
…
```
theorem OAI.CirculantHadamard.scalar_division_iff line 46
theorem OAI.CirculantHadamard.scalar_mul_left_cancel line 62
Source documentation
A scalar is cancellable because its action at each coefficient is injective. No domain structure is asserted for the group algebra.
```
theorem scalar_mul_left_cancel (p : R) (hp : p ≠ 0)
    {F K : AddMonoidAlgebra R G}
    (h : AddMonoidAlgebra.single (0 : G) p * F =
      AddMonoidAlgebra.single (0 : G) p * K) : F = K := by
…
```
theorem OAI.CirculantHadamard.scalar_mul_left_injective line 73

theorem OAI.CirculantHadamard.scalar_division_unique line 79

Source documentation

The element obtained by coefficientwise division is unique.

theorem scalar_division_unique (p : R) (hp : p ≠ 0)
    {F F₁ F₂ : AddMonoidAlgebra R G}
    (h₁ : F = AddMonoidAlgebra.single (0 : G) p * F₁)
    (h₂ : F = AddMonoidAlgebra.single (0 : G) p * F₂) : F₁ = F₂ :=
…

theorem OAI.CirculantHadamard.scalar_mul_norm_division line 87

Source documentation

Cancelling one regular scalar lowers the exponent of the norm equation by exactly one. This is valid although the group algebra has zero divisors.

theorem scalar_mul_norm_division (p : R) (hp : p ≠ 0) (e : ℕ) (b : R)
    (F K : AddMonoidAlgebra R G)
    (h : (AddMonoidAlgebra.single (0 : G) p * F) * K =
      AddMonoidAlgebra.single (0 : G) (p ^ (e + 1) * b)) :
    F * K = AddMonoidAlgebra.single (0 : G) (p ^ e * b) := by
…

theorem OAI.CirculantHadamard.quotient_scalar_norm_division line 111

Source documentation

Project the norm equation along a genuine ring homomorphism and then divide the chosen projected factor by one coefficient scalar.

theorem quotient_scalar_norm_division
    (q : AddMonoidAlgebra R G →+* AddMonoidAlgebra R H)
    (hscalar : ∀ r : R, q (AddMonoidAlgebra.single (0 : G) r) =
      AddMonoidAlgebra.single (0 : H) r)
    (p : R) (hp : p ≠ 0) (e : ℕ) (b : R)
    (F K : AddMonoidAlgebra R G) (F' : AddMonoidAlgebra R H)
    (hFK : F * K = AddMonoidAlgebra.single (0 : G) (p ^ (e + 1) * b))
    (hF : q F = AddMonoidAlgebra.single (0 : H) p * F') :
    F' * q K = AddMonoidAlgebra.single (0 : H) (p ^ e * b) := by
…