Zulip Chat Archive

Stream: mathlib4

Topic: porting notes

Johan Commelin (Apr 07 2025 at 16:46):

#23795 chore(LinearAlgebra): process misc porting notes

5 files changed, 12 insertions(+), 36 deletions(-)

Jireh Loreaux (Apr 07 2025 at 21:08):

build failing because of the principal' decl.

Johan Commelin (Apr 08 2025 at 04:23):

CI is happy now (-;

Johan Commelin (Apr 08 2025 at 09:31):

chore(LinearAlgebra): process misc porting notes #23809

16 files changed, 39 insertions(+), 142 deletions(-)

Johan Commelin (Apr 08 2025 at 12:22):

chore(Order): process misc porting notes #23825

9 files changed, 25 insertions(+), 43 deletions(-)

Johan Commelin (Apr 10 2025 at 06:37):

CI is now happy with :up:

Johan Commelin (Apr 10 2025 at 09:07):

#23908 chore(LinearAlgebra): process misc porting notes

7 files changed, 15 insertions(+), 49 deletions(-)

Last updated: May 02 2025 at 03:31 UTC