Zulip Chat Archive

Stream: new members

Topic: Integer def

Shadman Sakib (Jul 21 2021 at 21:50):

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

lemma integer_def : ∀ (n : ℤ), n ≤ 0  ∨ 1 ≤ n :=
begin
  intro n,
  sorry,
end

Shadman Sakib (Jul 21 2021 at 21:51):

Is there a lemma on mathlib that shows this? Library_Search can't seem to find it

Adam Topaz (Jul 21 2021 at 21:52):

library_search! gets it for me

Eric Rodriguez (Jul 21 2021 at 21:53):

whatever you're doing, it seems like cases n is much wiser

Adam Topaz (Jul 21 2021 at 21:53):

docs#le_or_lt

Shadman Sakib (Jul 21 2021 at 21:55):

Ah yeah, the exclamation mark makes the difference. Thank you!

Kevin Buzzard (Jul 21 2021 at 22:11):

cases n is breaking an abstraction barrier. Probably best to break into eg <= 0 and > 0 whilst keeping everything an integer

Last updated: Dec 20 2023 at 11:08 UTC