mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
--- [](https://gitpod.io/from-referrer/)
These were interesting when they worked on number literals, which is no longer the case in lean4. --- [](https://gitpod.io/from-referrer/)
For `Foo` an algebraic typeclass, the basic theory of `Subfoo` currently is under `FooTheory.Subfoo`. This is in contradiction to other kinds of subobjects, eg order theoretic ones. This PR moves...
* Make `Data.List.BigOperators.Basic`, `Data.List.Chain` not depend on `Data.Nat.Order.Basic` by using `Nat`-specific Std lemmas rather than general mathlib ones. I leave the `Data.Nat.Basic` import since `Data.List.BigOperators.Basic` is algebra territory. * As...
- krull dimension, height, coheight interacting with functions - order dual These will be specialized to ring theoretic krull dimension later --- - [ ] depends on:#11730 [](https://gitpod.io/from-referrer/)
* Make `Data.List.Count`, `Data.List.Dedup`, `Data.List.ProdSigma`, `Data.List.Range`, `Data.List.Rotate`, `Data.List.Zip` not depend on `Data.List.BigOperators.Basic`. * As a consequence, move the big operators lemmas that were in there to `Data.List.BigOperators.Basic`. For the lemmas...
feat(Algebra/Ring/Ext): prove extensionality lemmas for `Ring` and similar typeclasses Add file `Algebra/Ring/Ext`, proving `ext` lemmas for all of the ring-like classes (for example, anything from `NonUnitalNonAssocSemiring` to `CommRing`), stating that...
- add the theorem `image_restrictPreimage`; use it to simplify the proof of `Set.restrictPreimage_isClosedMap` - add the equivalent for open maps `Set.restrictPreimage_isOpenMap`. - delete `IsClosedMap.restrictPreimage`, which duplicates `Set.restrictPreimage_isClosedMap` --- This PR...
`Real.pow_sum_div_card_le_sum_pow` and `NNReal.pow_sum_div_card_le_sum_pow` both state that `(∑ i in s, f i) ^ (n + 1) / s.card ^ n ≤ ∑ i in s, f i ^ (n +...
This was previously about LinearOrderedRing, which is strictly stronger. The new assumptions match sq_nonneg. --- [](https://gitpod.io/from-referrer/)