leanprover-community/mathlib4 issues and pull requests

#50 - chore(*): update to nightly-2021-09-24

Pull Request - State: closed - Opened by semorrison about 3 years ago

#50 - chore(*): update to nightly-2021-09-24

Pull Request - State: closed - Opened by semorrison about 3 years ago

#49 - refactor(Tactic/NormNum): change to isNat function

Pull Request - State: closed - Opened by digama0 about 3 years ago

#49 - refactor(Tactic/NormNum): change to isNat function

Pull Request - State: closed - Opened by digama0 about 3 years ago

#48 - [Merged by Bors] - feat: add Init/Data/Nat/Basic.lean and Init/Data/Nat/Lemmas.lean

Pull Request - State: closed - Opened by dwrensha about 3 years ago - 3 comments

#48 - [Merged by Bors] - feat: add Init/Data/Nat/Basic.lean and Init/Data/Nat/Lemmas.lean

Pull Request - State: closed - Opened by dwrensha about 3 years ago - 3 comments

#47 - update lean to nightly-2021-08-29

Pull Request - State: closed - Opened by dwrensha about 3 years ago - 1 comment

#47 - update lean to nightly-2021-08-29

Pull Request - State: closed - Opened by dwrensha about 3 years ago - 1 comment

#46 - update lean version

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#46 - update lean version

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#45 - port init/algebra/functions.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#45 - port init/algebra/functions.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#44 - [Merged by Bors] - feat(Tactic/ShowTerm): port of show_term

Pull Request - State: closed - Opened by semorrison over 3 years ago - 4 comments

#44 - [Merged by Bors] - feat(Tactic/ShowTerm): port of show_term

Pull Request - State: closed - Opened by semorrison over 3 years ago - 4 comments

#43 - [Merged by Bors] - feat(Tactic/SolveByElim): minimal implementation

Pull Request - State: closed - Opened by semorrison over 3 years ago - 4 comments
Labels: awaiting-review

#43 - [Merged by Bors] - feat(Tactic/SolveByElim): minimal implementation

Pull Request - State: closed - Opened by semorrison over 3 years ago - 4 comments
Labels: awaiting-review

#42 - update lean version to nightly-2021-08-24

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 2 comments
Labels: awaiting-review

#42 - update lean version to nightly-2021-08-24

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 2 comments
Labels: awaiting-review

#41 - performance improvement for ring and normNum simplification on both sides

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago

#41 - performance improvement for ring and normNum simplification on both sides

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago

#40 - CommRing ℤ instance

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago

#40 - CommRing ℤ instance

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago

#39 - Ring tactic fix

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago - 1 comment

#39 - Ring tactic fix

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago - 1 comment

#38 - Abel tactic

Pull Request - State: closed - Opened by ChrisHughes24 over 3 years ago - 4 comments
Labels: WIP

#38 - Abel tactic

Pull Request - State: closed - Opened by ChrisHughes24 over 3 years ago - 4 comments
Labels: WIP

#37 - Expand ↑-notation.

Pull Request - State: closed - Opened by gebner over 3 years ago

#37 - Expand ↑-notation.

Pull Request - State: closed - Opened by gebner over 3 years ago

#36 - port remaining items from 'section propositional' in logic/basic

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#36 - port remaining items from 'section propositional' in logic/basic

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#35 - move Mathlib/Algebra/Order.lean to Mathlib/Init/Algebra/Order.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 1 comment

#35 - move Mathlib/Algebra/Order.lean to Mathlib/Init/Algebra/Order.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 1 comment

#34 - split out Lean 3 prelude items from Logic/Basic.lean into Init/Logic.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#34 - split out Lean 3 prelude items from Logic/Basic.lean into Init/Logic.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#33 - ring tactic

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago - 5 comments

#33 - ring tactic

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago - 5 comments

#32 - update lean to nightly-2021-08-11

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 3 comments

#32 - update lean to nightly-2021-08-11

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 3 comments

#31 - update lean to nightly-2021-08-06

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#31 - update lean to nightly-2021-08-06

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#30 - Tactic implementations

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago

#30 - Tactic implementations

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago

#29 - feat(Data/Subtype): port data/subtype.lean from mathlib3

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 4 comments

#29 - feat(Data/Subtype): port data/subtype.lean from mathlib3

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 4 comments

#28 - feat(Data/Prod) port data/prod.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#28 - feat(Data/Prod) port data/prod.lean

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#27 - Few tactic implementations

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago - 1 comment

#27 - Few tactic implementations

Pull Request - State: closed - Opened by AurelienSaue over 3 years ago - 1 comment

#26 - feat(Logic/Function/Basic) port most remaining items

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#26 - feat(Logic/Function/Basic) port most remaining items

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#25 - feat(Data/List/Card): add a theory of cardinality for lists

Pull Request - State: closed - Opened by avigad over 3 years ago

#25 - feat(Data/List/Card): add a theory of cardinality for lists

Pull Request - State: closed - Opened by avigad over 3 years ago

#24 - feat(Logic/Function/Basic) port everything up to partial_inv_left

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#24 - feat(Logic/Function/Basic) port everything up to partial_inv_left

Pull Request - State: closed - Opened by dwrensha over 3 years ago

#23 - feat(Data/Int): port data.int.basic from the lean3 prelude

Pull Request - State: closed - Opened by denayd over 3 years ago - 5 comments

#23 - feat(Data/Int): port data.int.basic from the lean3 prelude

Pull Request - State: closed - Opened by denayd over 3 years ago - 5 comments

#22 - feat(Data/List/Basic): start porting from mathlib

Pull Request - State: closed - Opened by avigad over 3 years ago

#22 - feat(Data/List/Basic): start porting from mathlib

Pull Request - State: closed - Opened by avigad over 3 years ago

#21 - fix: `matches` is now a keyword

Pull Request - State: closed - Opened by Vtec234 over 3 years ago

#21 - fix: `matches` is now a keyword

Pull Request - State: closed - Opened by Vtec234 over 3 years ago

#20 - port data/nat/gcd.lean (except for pow_dvd_pow_iff)

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 1 comment

#20 - port data/nat/gcd.lean (except for pow_dvd_pow_iff)

Pull Request - State: closed - Opened by dwrensha over 3 years ago - 1 comment

#19 - Create README.md

Pull Request - State: closed - Opened by jcommelin over 3 years ago

#19 - Create README.md

Pull Request - State: closed - Opened by jcommelin over 3 years ago

#18 - feat (Algebra): port init.algebra.order

Pull Request - State: closed - Opened by denayd over 3 years ago

#18 - feat (Algebra): port init.algebra.order

Pull Request - State: closed - Opened by denayd over 3 years ago

#17 - WIP: Digits lemmas for natural integers (port from mathlib3)

Pull Request - State: closed - Opened by RaitoBezarius over 3 years ago

#17 - WIP: Digits lemmas for natural integers (port from mathlib3)

Pull Request - State: closed - Opened by RaitoBezarius over 3 years ago

#16 - List: add missing repeat from Prelude

Pull Request - State: closed - Opened by RaitoBezarius over 3 years ago

#16 - List: add missing repeat from Prelude

Pull Request - State: closed - Opened by RaitoBezarius over 3 years ago

#15 - nat: Semiring instance for natural integers

Pull Request - State: closed - Opened by RaitoBezarius over 3 years ago - 1 comment

#15 - nat: Semiring instance for natural integers

Pull Request - State: closed - Opened by RaitoBezarius over 3 years ago - 1 comment

#14 - port int/basic.lean from lean3's core

Pull Request - State: closed - Opened by denayd over 3 years ago - 2 comments

#14 - port int/basic.lean from lean3's core

Pull Request - State: closed - Opened by denayd over 3 years ago - 2 comments

#13 - feat (Data/Equiv/Basic): add `equiv`

Pull Request - State: closed - Opened by kbuzzard over 3 years ago

#13 - feat (Data/Equiv/Basic): add `equiv`

Pull Request - State: closed - Opened by kbuzzard over 3 years ago

#12 - add Mem notation for lists

Pull Request - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#12 - add Mem notation for lists

Pull Request - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#11 - Mem instance for lists

Issue - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#11 - Mem instance for lists

Issue - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#10 - Improve module docstring for Set.lean

Pull Request - State: closed - Opened by PatrickMassot over 3 years ago - 1 comment

#10 - Improve module docstring for Set.lean

Pull Request - State: closed - Opened by PatrickMassot over 3 years ago - 1 comment

#9 - feat(Set): Add set notation for finite sets

Pull Request - State: closed - Opened by shingtaklam1324 over 3 years ago

#9 - feat(Set): Add set notation for finite sets

Pull Request - State: closed - Opened by shingtaklam1324 over 3 years ago

#8 - feat(Set): port Lean 3 init.data.set

Pull Request - State: closed - Opened by kbuzzard over 3 years ago

#8 - feat(Set): port Lean 3 init.data.set

Pull Request - State: closed - Opened by kbuzzard over 3 years ago

#7 - feat(Algebra/Group/Defs): add DivInvMonoid

Pull Request - State: closed - Opened by kbuzzard over 3 years ago

#7 - feat(Algebra/Group/Defs): add DivInvMonoid

Pull Request - State: closed - Opened by kbuzzard over 3 years ago

#6 - add some core Lean 3 `set` stuff and also `div_inv_monoid`

Pull Request - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#6 - add some core Lean 3 `set` stuff and also `div_inv_monoid`

Pull Request - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#5 - readme needed to introduce what this repo is about?

Issue - State: closed - Opened by brando90 over 3 years ago - 2 comments

#5 - readme needed to introduce what this repo is about?

Issue - State: closed - Opened by brando90 over 3 years ago - 2 comments

#4 - feat(Algebra/*): beginning of algebra heirarchy

Pull Request - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#4 - feat(Algebra/*): beginning of algebra heirarchy

Pull Request - State: closed - Opened by kbuzzard over 3 years ago - 1 comment

#3 - Add a LICENSE

Pull Request - State: closed - Opened by Julian over 3 years ago - 4 comments

#3 - Add a LICENSE

Pull Request - State: closed - Opened by Julian over 3 years ago - 4 comments

#2 - needs a LICENSE

Issue - State: closed - Opened by dwrensha over 3 years ago

#1 - refactor(leanpkg.toml): add plugin support

Pull Request - State: closed - Opened by gebner over 3 years ago

GitHub / leanprover-community/mathlib4 issues and pull requests