mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Quoting the docstring: `fast_instance% inst` takes an expression for a typeclass instance `inst`, and unfolds it into constructor applications that leverage existing instances. For instance, when used as ```lean instance...
Now that I am defining `NNRat.cast`, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use `natCast`/`intCast`/`ratCast` over `nat_cast`/`int_cast`/`rat_cast`, and this matches with the...
This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy. Reduce the diff of...
This PR extends the Hales-Jewett theorem from combinatorial lines to higher-dimensional combinatorial subspaces. It's an example of a theorem proving its own generalisation. Co-authored-by: David Wärn --- The plan is...
This changes the argument order for `cfc` and `cfcₙ` from `cfc (a : A) (f : R → R)` to `cfc (f : R → R) (a : A)`. This...
Construct a basis of a `PiTensorProduct` of modules given bases of the modules, and relationship between the dual of a `PiTensorProduct` and the `PiTensorProduct` of the duals. Main results: *...
This does three things: * `MultilinearMap.fromDirectSumEquiv` (in `LinearAlgebra/MultilinearMap/DirectSum.lean`) calculates `MultilinearMap`s on a family of `DirectSum`s. More precisely, if 'ι` is a `Fintype`, if `κ i` is a family of types...
--- - [x] depends on: #10661 - [ ] depends on: #10796 [](https://gitpod.io/from-referrer/)
--- Testing if Lean 4 can deal with this kind of instances. I'm going to wait for CI, then bench this PR. [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)