feat(*): Miscellaneous lemmas in algebra #1188
Conversation
| @@ -304,6 +304,14 @@ theorem sup_mul : (I ⊔ J) * K = I * K ⊔ J * K := | |||
| submodule.sup_smul I J K | |||
| variables {I J K} | |||
|
|
|||
| lemma pow_le_pow {m n : ℕ} (h : m ≤ n) : | |||
| I^n ≤ I^m := | |||
There was a problem hiding this comment.
Should this be called something with mono in ?
There was a problem hiding this comment.
I guess that would make sense... but there are a lot of other lemmas with pow_le_pow in their name in mathlib. @digama0 Which convention would you prefer?
@cipher1024 Is this something that should be tagged with @[mono] or something like that?
There was a problem hiding this comment.
Are ideals an ordered semiring?
There was a problem hiding this comment.
Good point, I'll look into proving it tomorrow. (I guess submodules form an ordered semiring, and in the case of ideals everything is ≤ 1).
There was a problem hiding this comment.
@ChrisHughes24 Hmm, they are not.
https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/library/init/algebra/ordered_group.lean#L21 is not satisfied. Take any I and J, then 1 = I + 1 ≤ J + 1 = 1, but we can't conclude I ≤ J.
ChrisHughes24
added
the
ready-to-merge
* Trying things out * feat(ring_theory/*): Misc little lemmas * More little lemmas
A bunch of tiny little lemmas, and some missing
to_additiveattributes.Mostly from the perfectoid project.