Zulip Chat Archive

Stream: general

Topic: proposed lemmas for mathlib


Scott Morrison (Oct 23 2019 at 05:00):

I'd like to add

lemma min_fac_le_div {n : ℕ} (pos : 0 < n) (np : ¬ prime n) : min_fac n ≤ n / min_fac n := ...

to mathlib.

I have an (almost-surely-pessimal) proof, so I'm not asking about that for now, just asking about suitability for mathlib.

Scott Morrison (Oct 23 2019 at 05:00):

One could make an iff version too.

Johan Commelin (Oct 23 2019 at 05:45):

Seems legit

Reid Barton (Oct 23 2019 at 11:17):

What's the iff version?

Reid Barton (Oct 23 2019 at 11:18):

I hope your proof begins apply min_fac_le_of_dvd,

Johan Commelin (Oct 23 2019 at 11:28):

I guess : ¬ prime n \iff min_fac n ≤ n / min_fac n

Reid Barton (Oct 24 2019 at 01:07):

Oh that makes sense. I was imaging something like "p is the minimum factor of n if and only if ..." and got stuck.


Last updated: Dec 20 2023 at 11:08 UTC