mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
... from requiring `F` being a field to `F` satisfying `StrongRankCondition` and `S` being a free `F`-module. This makes the original statement a special case. The changed results are: `Subalgebra.eq_bot_of_(rank_le|finrank)_one`,...
Golf & generalize `smul_top_eq_map`. --- [](https://gitpod.io/from-referrer/)
Misc lemmas about smul actions on submodules. --- The overall API of elements/sets/ideals acting on submodules kind of needs of an overhaul. There's a lot of stuff duplicated between these...
A Lean-linter implementation of the `#`-command linter introduced in #10809. This linter produces a warning whenever a non-whitelisted `#`-commands is used. The whitelist consists of `#align, #align_import, #noalign`. This PR...
--- - [x] depends on: #10814 - [ ] depends on: #10843 [](https://gitpod.io/from-referrer/)
Image of bilinear map in terms of tensor product. --- [](https://gitpod.io/from-referrer/)
Tensoring with the action of a scalar gives the action of that scalar. --- [](https://gitpod.io/from-referrer/)
Maximal ideal of local ring is contained in the jacobson radical of any ideal. --- [](https://gitpod.io/from-referrer/)
This PR adds the lemma claiming that if `X` and `Y` are independent and `(X, Y)` and `(X', Y')` are identically distributed, then `X'` and `Y'` are independent. See the...
To go with Matrix.det_permutation --- Question: this adds several imports to state the theorem. Should it be put elsewhere? [](https://gitpod.io/from-referrer/)
