mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
--- [](https://gitpod.io/from-referrer/)
also move `lTensor_inj_iff_rTensor_inj` to `LinearMap` --- [](https://gitpod.io/from-referrer/)
Adds `modByMonic_eq_zero_iff_quotient_eq_zero` and `quotient_singleton_eq` --- [](https://gitpod.io/from-referrer/)
In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas. Ported from leanprover-community/mathlib/pull/16040. Co-authored-by: Jiale Miao Co-authored-by: Eric Wieser --- [](https://gitpod.io/from-referrer/) This PR is...
--- [](https://gitpod.io/from-referrer/)
--- - [ ] depends on: #12434 [part one: submodule version] - [x] depends on: #11635 - [x] depends on: #11598 [need `finsuppTensorFinsupp'_symm_single`] - [x] depends on: #11731 - [x]...
Order/SuccPred/Basic.lean: add `SuccOrder.ofLinearWellFoundedLT`, which puts a SuccOrder on an arbitrary well-ordered type. Also add the dual, `PredOrder` version. Add missing `pred` lemmas corresponding to existing `succ` lemmas. Order/SuccPred/Limit.lean: add `SuccOrder.limitRecOn`...
Define cocountable and cocardinal filters. Any feedback on the way these are phrased and written is more than welcome! --- [](https://gitpod.io/from-referrer/)
A construction by transfinite recursion, fairly standard in set theory, but I have yet to see similar arguments in mathlib. See [module docstring](https://github.com/leanprover-community/mathlib4/blob/Field_Card_Emb/Mathlib/SetTheory/Cardinal/FieldEmb.lean#L20-L137) for more details. I use some ad...
1. if $A$ is a noetherian graded ring, then $A_0$ is a noetherian subring of $A$ and $A$ is a finitely generated algebra over $A_0$, if $M$ is a finitely...
