New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(Data/Nat/Factorial): Use Std lemmas #11715
Conversation
Move basic `Nat` lemmas from `Data.Nat.Order.Basic` and `Data.Nat.Pow` to `Data.Nat.Defs`. Most proofs need adapting, but that's easily solved by replacing the general mathlib lemmas by the new Std `Nat`-specific lemmas and using `omega`.
bors merge |
Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib. The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.
lemma monotone_factorial : Monotone factorial := fun _ _ => factorial_le | ||
#align nat.monotone_factorial Nat.monotone_factorial | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Surely this doesn't belong in this file?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There's already stuff about orders in there and I don't really feel like creating a new file just for this one lemma. I'm not quite sure where Monotone
will stand in the upcoming sublibraries but I think it will be in Order
and not imported by Nat.factorial
.
I'm happy for you to open a PR creating that Data.Nat.Factorial.Order
file if you want though, or maybe it can be in Data.Nat.Order.Lemmas
. Up to you.
Pull request successfully merged into master. Build succeeded: |
tendsto_atTop_atTop_of_monotone Nat.monotone_factorial fun n ↦ ⟨n, n.self_le_factorial⟩ | ||
tendsto_atTop_atTop_of_monotone (fun _ _ ↦ Nat.factorial_le) fun n ↦ ⟨n, n.self_le_factorial⟩ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would have thought you should just import monotone_factorial
here; it's very weird to consider Tendsto
more elementary than Monotone
IMO.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah sorry, that's an accident. I had originally put monotone_factorial
in Data.Nat.Factorial.Cast
, so I didn't put to import it in Analysis.SpecificLimits.Basic
.
Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib. The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.
Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib. The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.
Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib. The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.
Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib. The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.
Make use of
Nat
-specific lemmas from Std rather than the general ones provided by mathlib.The ultimate goal here is to carve out
Data
,Algebra
andOrder
sublibraries.