Documentation

FltRegular.NumberTheory.Cyclotomic.UnitLemmas

@[simp]

theorem coe_zpow' {K : Type u_1} [Field K] (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (n : ℤ) :

↑↑(u ^ n) = ↑↑u ^ n

theorem auxil {K : Type u_1} [Field K] (a : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (b : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (c : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (d : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (h : a * b⁻¹ = c * d) :

a * d⁻¹ = b * c

@[simp]

theorem IsPrimitiveRoot.val_unit'_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

↑↑(IsPrimitiveRoot.unit' hζ) = ζ

@[simp]

theorem IsPrimitiveRoot.val_inv_unit'_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

↑↑(IsPrimitiveRoot.unit' hζ)⁻¹ = ζ⁻¹

def IsPrimitiveRoot.unit' {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

{ x // x ∈ NumberField.ringOfIntegers K }ˣ

zeta now as a unit in the ring of integers. This way there are no coe issues

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem IsPrimitiveRoot.coe_unit'_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

↑↑(IsPrimitiveRoot.unit' hζ) = ζ

@[simp]

theorem IsPrimitiveRoot.coe_inv_unit'_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

↑↑(IsPrimitiveRoot.unit' hζ)⁻¹ = ζ⁻¹

@[simp]

theorem IsPrimitiveRoot.unit'_val_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

↑↑(IsPrimitiveRoot.unit' hζ) = ζ

theorem IsPrimitiveRoot.unit'_pow {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

IsPrimitiveRoot.unit' hζ ^ ↑p = 1

theorem zeta_runity_pow_even {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (hpo : Odd ↑p) (n : ℕ) :

∃ m, IsPrimitiveRoot.unit' hζ ^ n = IsPrimitiveRoot.unit' hζ ^ (2 * m)

theorem IsPrimitiveRoot.unit'_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] :

IsPrimitiveRoot ↑(IsPrimitiveRoot.unit' hζ) ↑p

def IsGalConjReal (p : ℕ+) {K : Type u_1} [Field K] [NumberField K] (x : K) [IsCyclotomicExtension {p} ℚ K] :

is_gal_conj_real x means that x is real.

Equations

IsGalConjReal p x = (↑(galConj K p) x = x)

Instances For

theorem contains_two_primitive_roots {K : Type u_1} [Field K] [NumberField K] {p : ℕ} {q : ℕ} {x : K} {y : K} [FiniteDimensional ℚ K] (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q) :

Nat.totient (lcm p q) ≤ FiniteDimensional.finrank ℚ K

theorem totient_le_one_dvd_two {a : ℕ} (han : 0 < a) (ha : Nat.totient a ≤ 1) :

a ∣ 2

theorem eq_one_mod_one_sub {A : Type u_1} [CommRing A] {t : A} :

↑(algebraMap A (A ⧸ Ideal.span {t - 1})) t = 1

theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {p : ℕ+} {A : Type u_1} [CommRing A] [IsDomain A] {ζ : A} (hζ : IsPrimitiveRoot ζ ↑p) {μ : A} (hμ : μ ^ ↑p = 1) :

↑(algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ = 1

instance instAlgebraSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersQuotientIdealToSemiringInstHasQuotientIdealToSemiringToCommSemiringToCommRingSpanSingletonSetInstSingletonSetHSubInstHSubSubToSubNegMonoidToAddGroupToAddGroupWithOneAddSubgroupClassInstSubringClassSubalgebraToCommSemiringToSemiringInstSetLikeSubalgebraValToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringUnit'OfNatToCommSemiringToCommSemiringCommRing {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

Algebra { x // x ∈ NumberField.ringOfIntegers K } ({ x // x ∈ NumberField.ringOfIntegers K } ⧸ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})

Equations

One or more equations did not get rendered due to their size.

instance instAddCommMonoidSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegers {K : Type u_1} [Field K] :

AddCommMonoid { x // x ∈ NumberField.ringOfIntegers K }

Equations

One or more equations did not get rendered due to their size.

instance instAddCommMonoidQuotientSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersIdealToSemiringInstHasQuotientIdealToSemiringToCommSemiringToCommRingSpanSingletonSetInstSingletonSetHSubInstHSubSubToSubNegMonoidToAddGroupToAddGroupWithOneAddSubgroupClassInstSubringClassSubalgebraToCommSemiringToSemiringInstSetLikeSubalgebraValToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringUnit'OfNat {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

AddCommMonoid ({ x // x ∈ NumberField.ringOfIntegers K } ⧸ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})

Equations

One or more equations did not get rendered due to their size.

theorem aux {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] {t : ℕ} {l : { x // x ∈ NumberField.ringOfIntegers K }} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ ↑p) (h : (Finset.sum Finset.univ fun x => f x • { val := μ, property := (_ : IsIntegral ℤ μ) } ^ ↑x) = l) :

↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } ({ x // x ∈ NumberField.ringOfIntegers K } ⧸ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})) l = Finset.sum Finset.univ fun x => ↑(f x)

theorem IsPrimitiveRoot.p_mem_one_sub_zeta {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [hp : Fact (Nat.Prime ↑p)] :

↑↑p ∈ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1}

theorem roots_of_unity_in_cyclo_aux {p : ℕ+} {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] {x : K} {n : ℕ} {l : ℕ} (hl : l ∈ Nat.divisors n) (hx : x ∈ NumberField.ringOfIntegers K) (hhl : Polynomial.IsRoot (Polynomial.cyclotomic l { x // x ∈ NumberField.ringOfIntegers K }) { val := x, property := hx }) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) :

l ∣ 2 * ↑p

theorem roots_of_unity_in_cyclo {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hpo : Odd ↑p) (x : K) (h : ∃ n x, x ^ n = 1) :

∃ m k, x = (-1) ^ ↑k * ↑↑(IsPrimitiveRoot.unit' hζ) ^ m

theorem norm_cast_ne_two {p : ℕ+} (h : p ≠ 2) :

↑p ≠ 2

theorem IsPrimitiveRoot.isPrime_one_sub_zeta {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] [hp : Fact (Nat.Prime ↑p)] (h : p ≠ 2) :

Ideal.IsPrime (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})

theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] [hp : Fact (Nat.Prime ↑p)] (h : p ≠ 2) :

¬2 ∈ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1}

theorem IsUnit.eq_mul_left_iff {S : Type u_1} [CommRing S] {x : S} (hx : IsUnit x) (y : S) :

x = y * x ↔ y = 1

theorem map_two {S : Type u_1} {T : Type u_2} {F : Type u_3} [NonAssocSemiring S] [NonAssocSemiring T] [RingHomClass F S T] (f : F) :

↑f 2 = 2

theorem neg_one_eq_one_iff_two_eq_zero {M : Type u_1} [AddGroupWithOne M] :

-1 = 1 ↔ 2 = 0

theorem Units.coe_map_inv' {M : Type u_1} {N : Type u_2} {F : Type u_3} [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) (m : Mˣ) :

↑(↑(Units.map ↑f) m)⁻¹ = ↑f ↑m⁻¹

theorem unit_inv_conj_not_neg_zeta_runity_aux {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (hp : Nat.Prime ↑p) :

↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } ({ x // x ∈ NumberField.ringOfIntegers K } ⧸ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})) ↑(u * (↑(unitGalConj K p) u)⁻¹) = 1

theorem unit_inv_conj_not_neg_zeta_runity {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (h : p ≠ 2) (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (n : ℕ) (hp : Nat.Prime ↑p) :

u * (↑(unitGalConj K p) u)⁻¹ ≠ -IsPrimitiveRoot.unit' hζ ^ n

theorem unit_inv_conj_is_root_of_unity {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (h : p ≠ 2) (hp : Nat.Prime ↑p) (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) :

∃ m, u * (↑(unitGalConj K p) u)⁻¹ = (IsPrimitiveRoot.unit' hζ ^ m) ^ 2

theorem inv_coe_coe {K : Type u_1} {A : Type u_2} [Field K] [SetLike A K] [SubsemiringClass A K] {S : A} (s : { x // x ∈ S }ˣ) :

(↑↑s)⁻¹ = ↑↑s⁻¹

theorem unit_lemma_gal_conj {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (h : p ≠ 2) (hp : Nat.Prime ↑p) (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) :

∃ x n, IsGalConjReal p ↑↑x ∧ u = x * IsPrimitiveRoot.unit' hζ ^ n

theorem IsPrimitiveRoot.eq_one_mod_one_sub' {A : Type u_1} [CommRing A] [IsDomain A] {n : ℕ+} {ζ : A} (hζ : IsPrimitiveRoot ζ ↑n) {η : A} (hη : η ∈ Polynomial.nthRootsFinset (↑n) A) :

↑(Ideal.Quotient.mk (Ideal.span {ζ - 1})) η = 1