IntegerTwoLocal.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The integers localized at the prime two

The ring is the actual localization of ℤ at the complement of (2). Its maximal ideal is generated by the image of two, and its nonzero generator makes it a discrete valuation ring. The characteristic-zero and odd-unit interfaces refer to this concrete localization, without assuming any valuation facts.

def OAI.CirculantHadamard.IntegerTwoLocal.ideal line 24
Source documentation
The prime ideal (2) in the integers.
```
def ideal : Ideal ℤ := Ideal.span {(2 : ℤ)}
```
instance OAI.CirculantHadamard.IntegerTwoLocal.ideal_isPrime line 26
abbrev OAI.CirculantHadamard.IntegerTwoLocal.Ring line 31
Source documentation
The actual ring ℤ_(2).
```
abbrev Ring := Localization.AtPrime ideal
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.ideal
theorem OAI.CirculantHadamard.IntegerTwoLocal.isDomain line 34
Source documentation
The localization has no zero divisors.
```
theorem isDomain : IsDomain Ring := inferInstance
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
theorem OAI.CirculantHadamard.IntegerTwoLocal.isLocalRing line 37
Source documentation
The complement-of-prime localization is local.
```
theorem isLocalRing : IsLocalRing Ring := inferInstance
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
theorem OAI.CirculantHadamard.IntegerTwoLocal.algebraMap_injective line 40
Source documentation
Integer coefficients embed faithfully in the concrete localization.
```
theorem algebraMap_injective : Function.Injective (algebraMap ℤ Ring) :=
…
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
instance OAI.CirculantHadamard.IntegerTwoLocal.charZero line 43
instance OAI.CirculantHadamard.IntegerTwoLocal.isNoetherianRing line 47
Source documentation
Noetherianity is inherited from the integer ring by localization.
```
instance isNoetherianRing : IsNoetherianRing Ring :=
…
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
theorem OAI.CirculantHadamard.IntegerTwoLocal.maximalIdeal_eq_span line 52
Source documentation
The maximal ideal is exactly the principal ideal generated by two.
```
theorem maximalIdeal_eq_span :
    IsLocalRing.maximalIdeal Ring = Ideal.span {(2 : Ring)} := by
…
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
theorem OAI.CirculantHadamard.IntegerTwoLocal.two_ne_zero line 60
theorem OAI.CirculantHadamard.IntegerTwoLocal.two_not_isUnit line 62
instance OAI.CirculantHadamard.IntegerTwoLocal.isDiscreteValuationRing line 68
Source documentation
The concrete localization is a discrete valuation ring with uniformizer (two); this conclusion is obtained from its proved principal maximal ideal.
```
instance isDiscreteValuationRing : IsDiscreteValuationRing Ring :=
…
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
theorem OAI.CirculantHadamard.IntegerTwoLocal.mem_ideal_iff_even line 72
theorem OAI.CirculantHadamard.IntegerTwoLocal.isUnit_algebraMap_iff_odd line 76
Source documentation
Exactly the odd integers become units.
```
theorem isUnit_algebraMap_iff_odd (z : ℤ) :
    IsUnit (algebraMap ℤ Ring z) ↔ Odd z := by
…
```
Mentions: OAI.CirculantHadamard.IntegerTwoLocal.Ring
theorem OAI.CirculantHadamard.IntegerTwoLocal.isUnit_intCast_of_odd line 82
theorem OAI.CirculantHadamard.IntegerTwoLocal.isUnit_natCast_of_odd line 85