ResidueOneAssociation.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Association by a unit with residue one

This algebraic relation expresses the local comparison conclusion without introducing division in the coefficient ring. The scalar-cancellation lemmas require regularity explicitly; they do not give group rings a domain instance. For a local ring, the residue map is the quotient by its maximal ideal.

def OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated line 22
Source documentation
x differs from y by multiplication by a unit whose residue is one.
```
def ResidueOneAssociated (residue : S →+* k) (x y : S) : Prop :=
…
```
theorem OAI.CirculantHadamard.LocalComparison.residue_inv_eq_one line 25
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.refl line 35
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.symm line 39
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.trans line 45
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.residue_eq line 53
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.mul_left line 57
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.mul_left_iff line 66
Source documentation
A common regular scalar can be cancelled even if the ambient ring has zero divisors. This is the form used when comparing scalar-divided factors.
```
theorem mul_left_iff (residue : S →+* k) (hc : IsLeftRegular c) :
    ResidueOneAssociated residue (c * x) (c * y) ↔
      ResidueOneAssociated residue x y := by
…
```
Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.mul line 77
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.product_complement_of_regular line 89
Source documentation
With equal nonzero products, a comparison for one factor gives the inverse unit as comparison for the other factor. Only regularity of y is needed.
```
theorem product_complement_of_regular (h : ResidueOneAssociated residue x y)
    (hprod : x * x' = y * y') (hy : IsLeftRegular y) :
    ResidueOneAssociated residue x' y' := by
…
```
Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.product_complement line 103
Source documentation
The two-factor step used in the character-comparison base case.
```
theorem product_complement [IsDomain S] (h : ResidueOneAssociated residue x y)
    (hprod : x * x' = y * y') (hne : y * y' ≠ 0) :
    ResidueOneAssociated residue x' y' := by
…
```
Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.mul_left_iff_of_ne_zero line 109
theorem OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated.of_isUnit_of_residue_eq line 115
Source documentation
Two units with the same residue differ by a unit with residue one.
```
theorem of_isUnit_of_residue_eq (residue : S →+* k)
    (hx : IsUnit x) (hy : IsUnit y) (hres : residue x = residue y) :
    ResidueOneAssociated residue x y := by
…
```
Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated
theorem OAI.CirculantHadamard.LocalComparison.isUnit_of_residue_eq line 132
Source documentation
Equality to the residue of a unit forces an element of a local ring to be a unit. The residue map is the actual quotient by the maximal ideal.
```
theorem isUnit_of_residue_eq (hy : IsUnit y)
    (hres : IsLocalRing.residue S x = IsLocalRing.residue S y) : IsUnit x := by
…
```
theorem OAI.CirculantHadamard.LocalComparison.residueOneAssociated_of_isUnit_residue_eq line 140
Source documentation
Concrete local-ring base case: an augmentation unit and agreement in the residue field suffice to construct the comparison unit.
```
theorem residueOneAssociated_of_isUnit_residue_eq (hy : IsUnit y)
    (hres : IsLocalRing.residue S x = IsLocalRing.residue S y) :
    ResidueOneAssociated (IsLocalRing.residue S) x y :=
…
```
Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated