## Stream: new members

#### Shadman Sakib (Jul 25 2021 at 18:13):

The contradiction should be that since a : Z then a ≠ n would mean a is not in Z but Lean does not understand. How can I make this contradiction more explicit?

#### Shadman Sakib (Jul 25 2021 at 18:13):

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi

noncomputable theory

open complex dihedral_group

local notation | x | := complex.abs x
local notation π := real.pi

example (R : Type*) (n : ℤ) (θ : ℝ) (a : ℤ) (h : 2 ≠ 0)
(h₁ : 2 / π < 3 / π) (h₃ : 3 / π < 1)
[linear_ordered_ring R]
(this : ↑θ * I + I * -(↑θ / 2) = I * (↑θ / 2))
(ha : I * 2 + I * (↑θ / 2) =
-(I * 2) + I * (↑θ / 2) + ↑a * (2 * ↑π * I))
(this : (2 : ℂ) = ↑a * ↑π)
(h₀ : (a :ℂ) = 2 / π)
(h₂ : 0 < a)
(h₄ : a < 1)
(this₁ : a < 1 → 0 < a → ¬a = n)
(this₃ : ¬a = n) :
false :=
begin
end


#### Adam Topaz (Jul 25 2021 at 18:31):

I think you're misunderstanding something here... it looks like a and n are both terms of Z, so there is no contradiction in saying that a and n are different. However, you can get a contradiction from $0 and $a<1$ since a is an integer.

#### Shadman Sakib (Jul 25 2021 at 18:47):

Yes, I have a lemma that I proved showing that if 0 < a and a < 1 then a cannot equal any integer and this1 was the result. Lean will not let me create a have statement saying a is not in Z.

#### Shadman Sakib (Jul 25 2021 at 18:52):

Maybe this state will help

#### Shadman Sakib (Jul 25 2021 at 18:53):

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric
import data.real.pi

noncomputable theory

open complex dihedral_group

local notation | x | := complex.abs x
local notation π := real.pi

example (R : Type*) (n : ℤ) (θ : ℝ) (a : ℤ) (h : 2 ≠ 0)
(h₁ : 2 / π < 3 / π) (h₃ : 3 / π < 1)
[linear_ordered_ring R]
(this : ↑θ * I + I * -(↑θ / 2) = I * (↑θ / 2))
(ha : I * 2 + I * (↑θ / 2) =
-(I * 2) + I * (↑θ / 2) + ↑a * (2 * ↑π * I))
(this : (2 : ℂ) = ↑a * ↑π)
(h₀ : (a : ℂ) = 2 / π)
(h₂ : 0 < a)
(h₄ : a < 1)
(this₁ : ∀ (n : ℤ), a < 1 → 0 < a → ¬a = n) :
false :=
begin
end


#### Shadman Sakib (Jul 25 2021 at 18:54):

I introduced an n to this1, and applied this1 to h2 and h4, that is why in the previous #mwe this3 has a ≠ n

#### Adam Topaz (Jul 25 2021 at 18:59):

Saying "a is not in Z" when a : Z makes no sense in type theory.

#### Adam Topaz (Jul 25 2021 at 19:00):

It seems that this is an issue about understanding type theory, so I suggest looking at the relevant sections of #tpil

#### Adam Topaz (Jul 25 2021 at 19:01):

(i.e. ch. 2)

Last updated: Dec 20 2023 at 11:08 UTC