mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
This will need minor additions once the tactic `mono` is ported, and some additional testing after `Logic.Equiv.Basic` and `Order.Hom.Basic` are ported.
Porting anything trivial to port which contains lemmas mentioned by mathlib3's `norm_num` or `ring`.
This is still far from feature parity with mathlib3, but at least you can add custom expressions, and omit the local context.
This is a port of `fin_cases`. It doesn't yet support the `with` or `using` clauses from mathlib3. I could remove the dependence on #433, but would have to (temporarily) remove...
- [ ] depends on #470, for `OrderedRing`.
These aren't complete ports, mostly just the typeclass definition parts of * `Algebra.Order.Monoid` * `Algebra.Order.Group` * `Algebra.Order.Ring` Creating these typeclasses with sorried instances for use with `linarith` was barely easier...
This issue parallels the content of [`Mathlib/Mathport/Syntax.lean`][Syntax.lean], tracking the remaining work to port mathlib3 tactics to mathlib4, but also contains "ephemeral" information that does not belong in that file. Primarily,...
This PR is an almost complete rewrite of `norm_num` to implement its functionality via an extensible attribute for plugins, and use `Qq` for expression construction.
* This way we can add `@[to_additive]` attributes much easier via metaprogramming. * Useful for the `@[simps]` attribute
